let G be non empty multMagma ; :: thesis: 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; :: thesis: ( 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: H₂(H2) c= H₂(G) by Def23;
( H₂(H1) c= H₂(G) & dom H₂(H1) = [:H₁(H1),H₁(H1):] ) by Def23, FUNCT_2:def 1;
then A2: H₂(H1) = H₂(G) || H₁(H1) by GRFUNC_1:23;
assume A3: H₁(H1) = H₁(H2) ; :: thesis: multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
then dom H₂(H2) = [:H₁(H1),H₁(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; :: thesis: verum