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