theorem Th15: :: ALGSTR_4:15
for M, N being non empty multMagma
for f being Function of M,N
for X being Subset of M st f is multiplicative holds
f .: the carrier of (the_submagma_generated_by X) = the carrier of (the_submagma_generated_by (f .: X))