let G1, G2 be Group; :: thesis: for A1 being Subset of G1
for A2 being Subset of G2
for H1 being strict Subgroup of G1
for H2 being strict Subgroup of G2 st multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) & A1 = A2 & H1 = H2 holds
( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 )
let A1 be Subset of G1; :: thesis: for A2 being Subset of G2
for H1 being strict Subgroup of G1
for H2 being strict Subgroup of G2 st multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) & A1 = A2 & H1 = H2 holds
( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 )
let A2 be Subset of G2; :: thesis: for H1 being strict Subgroup of G1
for H2 being strict Subgroup of G2 st multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) & A1 = A2 & H1 = H2 holds
( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 )
let H1 be strict Subgroup of G1; :: thesis: for H2 being strict Subgroup of G2 st multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) & A1 = A2 & H1 = H2 holds
( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 )
let H2 be strict Subgroup of G2; :: thesis: ( multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) & A1 = A2 & H1 = H2 implies ( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 ) )
assume A1: multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) ; :: thesis: ( not A1 = A2 or not H1 = H2 or ( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 ) )

A2: now :: thesis: for A1, B1 being Subset of G1
for A2, B2 being Subset of G2 st A1 = A2 & B1 = B2 holds
{ (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 ) }

let A1, B1 be Subset of G1; :: thesis: for A2, B2 being Subset of G2 st A1 = A2 & B1 = B2 holds
{ (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 ) }
let A2, B2 be Subset of G2; :: thesis: ( A1 = A2 & B1 = B2 implies { (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 ) } )
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: { (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 ) }

A4: now :: thesis: for x being object st x in { (g * h) where g, h is Element of G1 : ( g in A1 & h in B1 ) } holds
x in { (g * h) where g, h is Element of G2 : ( g in A2 & h in B2 ) }

let x be object ; :: thesis: ( x in { (g * h) where g, h is Element of G1 : ( g in A1 & h in B1 ) } implies x in { (g * h) where g, h is Element of G2 : ( g in A2 & h in B2 ) } )
assume x in { (g * h) where g, h is Element of G1 : ( g in A1 & h in B1 ) } ; :: thesis: x in { (g * h) where g, h is Element of G2 : ( g in A2 & h in B2 ) }
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: verum

end;

now :: thesis: for x being object st x in { (g * h) where g, h is Element of G2 : ( g in A2 & h in B2 ) } holds
x in { (g * h) where g, h is Element of G1 : ( g in A1 & h in B1 ) }

let x be object ; :: thesis: ( x in { (g * h) where g, h is Element of G2 : ( g in A2 & h in B2 ) } implies x in { (g * h) where g, h is Element of G1 : ( g in A1 & h in B1 ) } )
assume x in { (g * h) where g, h is Element of G2 : ( g in A2 & h in B2 ) } ; :: thesis: x in { (g * h) where g, h is Element of G1 : ( g in A1 & h in B1 ) }
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: verum

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: verum

end;

assume A7: A1 = A2 ; :: thesis: ( not H1 = H2 or ( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 ) )
assume A8: H1 = H2 ; :: thesis: ( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 )
hence A1 * H1 = A2 * H2 by A7, A2; :: thesis: H1 * A1 = H2 * A2
thus H1 * A1 = H2 * A2 by A7, A8, A2; :: thesis: verum