theorem Th6: :: ALGSTR_4:6

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