let G1, G2 be Group; ( G1 is Subgroup of G2 & G2 is Subgroup of G1 implies multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) )
assume that
A1:
G1 is Subgroup of G2
and
A2:
G2 is Subgroup of G1
; multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #)
set g = the multF of G2;
set f = the multF of G1;
set B = the carrier of G2;
set A = the carrier of G1;
A3:
( the carrier of G1 c= the carrier of G2 & the carrier of G2 c= the carrier of G1 )
by A1, A2, Def5;
then A4:
the carrier of G1 = the carrier of G2
;
the multF of G1 =
the multF of G2 || the carrier of G1
by A1, Def5
.=
( the multF of G1 || the carrier of G2) || the carrier of G1
by A2, Def5
.=
the multF of G1 || the carrier of G2
by A4, RELAT_1:72
.=
the multF of G2
by A2, Def5
;
hence
multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #)
by A3, XBOOLE_0:def 10; verum