theorem Th41: :: ALGSTR_4:41

for M, N being non empty multMagma
for f being Function of M,N
for H being non empty multSubmagma of N
for R being compatible Equivalence_Relation of M st f is multiplicative & the carrier of H = rng f & R = equ_kernel f holds
ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) & g is bijective & g is multiplicative )