let M be non empty multMagma ; 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 Th39;
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;
the multF of M = the multF of M | [: the carrier of M, the carrier of M:]
;
then
the multF of M = the multF of M || the carrier of M
by REALSET1:def 2;
then reconsider H = M as non empty multSubmagma of M by Def9;
for y being object st y in the carrier of M holds
ex x being object st
( x in dom f & y = f . x )
proof
let y be
object ;
( y in the carrier of M implies ex x being object st
( x in dom f & y = f . x ) )
assume A3:
y in the
carrier of
M
;
ex x being object st
( x in dom f & y = f . x )
reconsider x =
[y,1] as
set ;
take
x
;
( x in dom f & y = f . x )
[:(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 Def13;
1
in {1}
by TARSKI:def 1;
then
x in [: the carrier of M,{1}:]
by A3, ZFMISC_1:def 2;
then
x in the
carrier of
(free_magma the carrier of M)
by A4;
hence
x in dom f
by FUNCT_2:def 1;
y = f . x
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;
A6:
(canon_image ( the carrier of M,1)) . y = x
by A3, Lm3;
y in dom (canon_image ( the carrier of M,1))
by A3, Lm3;
then
x in rng (canon_image ( the carrier of M,1))
by A6, FUNCT_1:3;
then A7:
x in dom ((canon_image ( the carrier of M,1)) ")
by FUNCT_1:33;
dom (canon_image ( the carrier of M,1)) c= dom (id the carrier of M)
by Lm3;
then
rng ((canon_image ( the carrier of M,1)) ") c= dom (id the carrier of M)
by FUNCT_1:33;
then A8:
x in dom ((id the carrier of M) * ((canon_image ( the carrier of M,1)) "))
by A7, RELAT_1:27;
A9:
y in dom (canon_image ( the carrier of M,1))
by A3, Lm3;
thus y =
(id the carrier of M) . y
by A3, FUNCT_1:18
.=
(id the carrier of M) . (((canon_image ( the carrier of M,1)) ") . x)
by A9, A6, FUNCT_1:34
.=
((id the carrier of M) * ((canon_image ( the carrier of M,1)) ")) . x
by A8, FUNCT_1:12
.=
f . x
by A8, A5, PARTFUN1:53
;
verum
end;
then
the carrier of M c= rng f
by FUNCT_1:9;
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, Th41;
reconsider g = g as Function of ((free_magma the carrier of M) ./. (equ_rel r)),M by A2;
take
the carrier of M
; 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
; ex g being Function of ((free_magma the carrier of M) ./. (equ_rel r)),M st
( g is bijective & g is multiplicative )
take
g
; ( g is bijective & g is multiplicative )
thus
( g is bijective & g is multiplicative )
by A10, A2; verum