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 ) )
assume A2: A1 = A2 ; :: thesis: ( not H1 = H2 or ( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 ) )
assume A3: H1 = H2 ; :: thesis: ( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 )

A4: now

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 ) } )
assume A5: ( 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 ) }
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 ) } ;

A6: now

let x be set ; :: 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
A7: ( x = g * h & g in A1 & h in B1 ) ;
set g' = g;
set h' = h;
reconsider g' = g, h' = h as Element of G2 by A1;
g * h = g' * h' by A1;
hence x in { (g * h) where g, h is Element of G2 : ( g in A2 & h in B2 ) } by A5, A7; :: thesis: verum

end;

now

let x be set ; :: 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
A8: ( x = g * h & g in A2 & h in B2 ) ;
reconsider g' = g, h' = h as Element of G1 by A1;
g * h = g' * h' by A1;
hence x in { (g * h) where g, h is Element of G1 : ( g in A1 & h in B1 ) } by A5, A8; :: 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 A6, TARSKI:2; :: thesis: verum

end;

hence A1 * H1 = A2 * H2 by A2, A3; :: thesis: H1 * A1 = H2 * A2
thus H1 * A1 = H2 * A2 by A2, A3, A4; :: thesis: verum