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

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 ) }

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

end;{ (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 ) }

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;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

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 ) }

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: verumx 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;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

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