let M be non empty multMagma ; :: thesis: ex X being non empty set ex r being Relators of (free_magma X) ex g being Function of ((free_magma X) ./. (equ_rel r)),M st
( g is bijective & g is multiplicative )
set X = the carrier of M;
consider f being Function of (free_magma the carrier of M),M such that
A1: ( f is multiplicative & f extends (id the carrier of M) * ((canon_image the carrier of M,1) " ) ) by Th40;
consider r being Relators of (free_magma the carrier of M) such that
A2: equ_kernel f = equ_rel r by A1, Th5;
reconsider R = equ_kernel f as compatible Equivalence_Relation of (free_magma the carrier of M) by A1, Th4;
dom the multF of M c= [:the carrier of M,the carrier of M:] ;
then the multF of M = the multF of M | [:the carrier of M,the carrier of M:] by RELAT_1:97;
then the multF of M = the multF of M || the carrier of M by REALSET1:def 3;
then reconsider H = M as non empty multSubmagma of M by Def10;
for y being set st y in the carrier of M holds
ex x being set st
( x in dom f & y = f . x )

proof

let y be set ; :: thesis: ( y in the carrier of M implies ex x being set st
( x in dom f & y = f . x ) )
assume A3: y in the carrier of M ; :: thesis: ex x being set st
( x in dom f & y = f . x )
set x = [y,1];
take [y,1] ; :: thesis: ( [y,1] in dom f & y = f . [y,1] )
[:(free_magma the carrier of M,1),{1}:] c= the carrier of (free_magma the carrier of M) by Lm1;
then A4: [:the carrier of M,{1}:] c= the carrier of (free_magma the carrier of M) by Def14;
1 in {1} by TARSKI:def 1;
then [y,1] in [:the carrier of M,{1}:] by A3, ZFMISC_1:def 2;
then [y,1] in the carrier of (free_magma the carrier of M) by A4;
hence [y,1] in dom f by FUNCT_2:def 1; :: thesis: y = f . [y,1]
A5: ( dom ((id the carrier of M) * ((canon_image the carrier of M,1) " )) c= dom f & f tolerates (id the carrier of M) * ((canon_image the carrier of M,1) " ) ) by A1, Def3;
A6: (canon_image the carrier of M,1) . y = [y,1] by A3, Lm2;
y in dom (canon_image the carrier of M,1) by A3, Lm2;
then [y,1] in rng (canon_image the carrier of M,1) by A6, FUNCT_1:12;
then A7: [y,1] in dom ((canon_image the carrier of M,1) " ) by FUNCT_1:55;
the carrier of M c= dom (id the carrier of M) by FUNCT_2:def 1;
then dom (canon_image the carrier of M,1) c= dom (id the carrier of M) by Lm2;
then rng ((canon_image the carrier of M,1) " ) c= dom (id the carrier of M) by FUNCT_1:55;
then A8: [y,1] in dom ((id the carrier of M) * ((canon_image the carrier of M,1) " )) by A7, RELAT_1:46;
A9: y in dom (canon_image the carrier of M,1) by A3, Lm2;
thus y = (id the carrier of M) . y by A3, FUNCT_1:35
.= (id the carrier of M) . (((canon_image the carrier of M,1) " ) . [y,1]) by A9, FUNCT_1:56, A6
.= ((id the carrier of M) * ((canon_image the carrier of M,1) " )) . [y,1] by A8, FUNCT_1:22
.= f . [y,1] by A8, A5, PARTFUN1:132 ; :: thesis: verum

end;

then the carrier of M c= rng f by FUNCT_1:19;
then the carrier of H = rng f by XBOOLE_0:def 10;
then consider g being Function of ((free_magma the carrier of M) ./. R),H such that
A10: ( f = g * (nat_hom R) & g is bijective & g is multiplicative ) by A1, Th42;
reconsider g = g as Function of ((free_magma the carrier of M) ./. (equ_rel r)),M by A2;
take the carrier of M ; :: thesis: ex r being Relators of (free_magma the carrier of M) ex g being Function of ((free_magma the carrier of M) ./. (equ_rel r)),M st
( g is bijective & g is multiplicative )
take r ; :: thesis: ex g being Function of ((free_magma the carrier of M) ./. (equ_rel r)),M st
( g is bijective & g is multiplicative )
take g ; :: thesis: ( g is bijective & g is multiplicative )
thus ( g is bijective & g is multiplicative ) by A10, A2; :: thesis: verum