defpred S_{1}[ set , set ] means ( $1 in M & $2 in N );

deffunc H_{1}( Element of V, Element of V) -> Element of the carrier of V = $1 + $2;

{ H_{1}(u,v) where u, v is Element of V : S_{1}[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

deffunc H

{ H

hence { (u + v) where u, v is Element of V : ( u in M & v in N ) } is Subset of V ; :: thesis: verum