defpred S₁[ set , set ] means ( $1 in X & $2 in Y );
deffunc H₁( Element of REAL , Element of REAL ) -> Element of REAL = $1 + $2;
{ H₁(r,r1) where r, r1 is Real : S₁[r,r1] } is Subset of REAL from COMPLSP1:sch 2();
hence { (r + r1) where r, r1 is Real : ( r in X & r1 in Y ) } is Subset of REAL ; :: thesis: verum