{\small\sf class} $Universitaet$
\par
\kInstanceVarDef
\parlinebr
\begin{insvar}
\assdef{Name}{\seqof*{\Char }}
\end{insvar}
\begin{instinvfn}
Name \Neq \Dquote  \Dquote \end{instinvfn}
\begin{insvar}
\assdef{Anschrift}{Adresse}
\end{insvar}
\begin{insvar}\kw{public}
\assdef{immat}{\Natone  \Bmap Immatrikulation}[{\Emptymap }]
\end{insvar}
\begin{instinvfn}
\all{i1,i2 \In  \Rng immat}{i1 \Neq i2 \Implies  \\
i1.MatrikelNummer \Neq i2.MatrikelNummer}\end{instinvfn}
\begin{instinvfn}
\all{i \In  \Rng immat}{i.uni = \kSelf }\end{instinvfn}
\begin{instinvfn}
\all{i \In  \Rng immat}{i = \fnapply{immat}{i.MatrikelNummer}}\end{instinvfn}
\begin{instinvfn}
\begin{letexpr}
\patdef{AllStuds}{\setcomp{i.stud}{i \In  \Rng immat}}
\end{letexpr} \\
\begin{letexpr}
\patdef{AllKursnoten}{ \Dunion \setcomp{ \Rng i.kursnote}{i \In AllStuds}}
\end{letexpr} \\
\all{p1,p2 \In AllKursnoten}{p1 \Neq p2 \Implies  \\
p1.Pruefungsnummer \Neq p2.Pruefungsnummer}\end{instinvfn}
\par
{\small\sf end} {\it Universitaet}

