defpred S₁[ set , set ] means ( $1 in M & $2 in N );
deffunc H₁( Element of V, Element of V) -> Element of the carrier of V = $1 + $2;
{ H₁(u,v) where u, v is Element of V : S₁[u,v] } is Subset of V from DOMAIN_1:sch 9();
hence { (u + v) where u, v is Element of V : ( u in M & v in N ) } is Subset of V ; :: thesis: verum