defpred S_{1}[ Element of G, Element of G] means ( $1 in A & $2 in B );

deffunc H_{1}( Element of G, Element of G) -> Element of G = [.$1,$2.];

{ H_{1}(a,b) where a, b is Element of G : S_{1}[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

deffunc H

{ H

hence { [.a,b.] where a, b is Element of G : ( a in A & b in B ) } is Subset of G ; :: thesis: verum