let G be non empty multMagma ; for H1, H2 being non empty SubStr of G st the carrier of H1 = the carrier of H2 holds
multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
let H1, H2 be non empty SubStr of G; ( the carrier of H1 = the carrier of H2 implies multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) )
A1:
H2(H2) c= H2(G)
by Def23;
( H2(H1) c= H2(G) & dom H2(H1) = [:H1(H1),H1(H1):] )
by Def23, FUNCT_2:def 1;
then A2:
H2(H1) = H2(G) || H1(H1)
by GRFUNC_1:23;
assume A3:
H1(H1) = H1(H2)
; multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
then
dom H2(H2) = [:H1(H1),H1(H1):]
by FUNCT_2:def 1;
hence
multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
by A3, A1, A2, GRFUNC_1:23; verum