theorem Th26: :: MONOID_0:26

for G being 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 #)