theorem Th7: :: ALGSTR_4:7

for M being multMagma
for N being multSubmagma of M st the carrier of N = the carrier of M holds
multMagma(# the carrier of N, the multF of N #) = multMagma(# the carrier of M, the multF of M #)