let G1, G2 be Group; :: thesis:
let A1 be Subset of G1; :: thesis:
let A2 be Subset of G2; :: thesis:
let H1 be strict Subgroup of G1; :: thesis:
let H2 be strict Subgroup of G2; :: thesis:
assume A1: multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) ; :: thesis:

let A1, B1 be Subset of G1; :: thesis:
let A2, B2 be Subset of G2; :: thesis:
set X = { (g * h) where g, h is Element of G1 : ( g in A1 & h in B1 ) } ;
set Y = { (g * h) where g, h is Element of G2 : ( g in A2 & h in B2 ) } ;
assume A3: ( A1 = A2 & B1 = B2 ) ; :: thesis:

let x be object ; :: thesis:
assume x in { (g * h) where g, h is Element of G1 : ( g in A1 & h in B1 ) } ; :: thesis:
then consider g, h being Element of G1 such that
A5: ( x = g * h & g in A1 & h in B1 ) ;
set h9 = h;
set g9 = g;
reconsider g9 = g, h9 = h as Element of G2 by A1;
g * h = g9 * h9 by A1;
hence x in { (g * h) where g, h is Element of G2 : ( g in A2 & h in B2 ) } by A3, A5; :: thesis:

end;

let x be object ; :: thesis:
assume x in { (g * h) where g, h is Element of G2 : ( g in A2 & h in B2 ) } ; :: thesis:
then consider g, h being Element of G2 such that
A6: ( x = g * h & g in A2 & h in B2 ) ;
reconsider g9 = g, h9 = h as Element of G1 by A1;
g * h = g9 * h9 by A1;
hence x in { (g * h) where g, h is Element of G1 : ( g in A1 & h in B1 ) } by A3, A6; :: thesis:

end;

hence { (g * h) where g, h is Element of G1 : ( g in A1 & h in B1 ) } = { (g * h) where g, h is Element of G2 : ( g in A2 & h in B2 ) } by A4, TARSKI:2; :: thesis:

end;

assume A7: A1 = A2 ; :: thesis:
assume A8: H1 = H2 ; :: thesis:
hence A1 * H1 = A2 * H2 by A7, A2; :: thesis:
thus H1 * A1 = H2 * A2 by A7, A8, A2; :: thesis: