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