defpred S₁[ Element of , Element of ] means ( $1 in A & $2 in B );
deffunc H₁( Element of , Element of ) -> Element of = [.$1,$2.];
{ H₁(a,b) where a, b is Element of : S₁[a,b] } is Subset of from DOMAIN_1:sch 9();
hence { [.a,b.] where a, b is Element of : ( a in A & b in B ) } is Subset of ; :: thesis: verum