let X, Y be non empty set ; for f being Function of X,Y st f is onto holds
free_magmaF f is onto
let f be Function of X,Y; ( f is onto implies free_magmaF f is onto )
assume A1:
f is onto
; free_magmaF f is onto
for y being object st y in the carrier of (free_magma Y) holds
y in rng (free_magmaF f)
proof
let y be
object ;
( y in the carrier of (free_magma Y) implies y in rng (free_magmaF f) )
assume A2:
y in the
carrier of
(free_magma Y)
;
y in rng (free_magmaF f)
defpred S1[
Nat]
means for
w being
Element of
(free_magma Y) st
length w = $1 holds
ex
v being
Element of
(free_magma X) st
w = (free_magmaF f) . v;
A3:
for
k being
Nat st ( for
n being
Nat st
n < k holds
S1[
n] ) holds
S1[
k]
proof
let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A4:
for
n being
Nat st
n < k holds
S1[
n]
;
S1[k]
thus
for
w being
Element of
(free_magma Y) st
length w = k holds
ex
v being
Element of
(free_magma X) st
w = (free_magmaF f) . v
verumproof
let w be
Element of
(free_magma Y);
( length w = k implies ex v being Element of (free_magma X) st w = (free_magmaF f) . v )
assume A5:
length w = k
;
ex v being Element of (free_magma X) st w = (free_magmaF f) . v
A6:
(
w = [(w `1),(w `2)] &
length w >= 1 )
by Th32;
then
(
length w = 1 or
length w > 1 )
by XXREAL_0:1;
then A7:
(
length w = 1 or
(length w) + 1
> 1
+ 1 )
by XREAL_1:8;
per cases
( length w = 1 or length w >= 2 )
by A7, NAT_1:13;
suppose A8:
length w = 1
;
ex v being Element of (free_magma X) st w = (free_magmaF f) . vset y =
w `1 ;
w `1 in { (w9 `1) where w9 is Element of (free_magma Y) : length w9 = 1 }
by A8;
then A9:
w `1 in Y
by Th30;
free_magmaF f extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ")
by Def21;
then A10:
(
dom (((canon_image (Y,1)) * f) * ((canon_image (X,1)) ")) c= dom (free_magmaF f) &
((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") tolerates free_magmaF f )
;
A11:
(canon_image (Y,1)) . (w `1) =
[(w `1),1]
by A9, Lm3
.=
w
by Def18, A6, A8
;
A12:
rng f = Y
by A1, FUNCT_2:def 3;
then consider x being
object such that A13:
(
x in dom f &
w `1 = f . x )
by A9, FUNCT_1:def 3;
A14:
1
in {1}
by TARSKI:def 1;
A15:
x in X
by A13;
then
x in free_magma (
X,1)
by Def13;
then A16:
[x,1] in [:(free_magma (X,1)),{1}:]
by A14, ZFMISC_1:def 2;
[:(free_magma (X,1)),{1}:] c= free_magma_carrier X
by Lm1;
then reconsider v =
[x,1] as
Element of
(free_magma X) by A16;
take
v
;
w = (free_magmaF f) . vA17:
x in dom (canon_image (X,1))
by Lm3, A15;
A18:
v = (canon_image (X,1)) . x
by Lm3, A13;
then
v in rng (canon_image (X,1))
by A17, FUNCT_1:3;
then A19:
v in dom ((canon_image (X,1)) ")
by FUNCT_1:33;
rng f = dom (canon_image (Y,1))
by Lm3, A12;
then
dom f = dom ((canon_image (Y,1)) * f)
by RELAT_1:27;
then
X c= dom ((canon_image (Y,1)) * f)
by FUNCT_2:def 1;
then
dom (canon_image (X,1)) c= dom ((canon_image (Y,1)) * f)
by Lm3;
then
rng ((canon_image (X,1)) ") c= dom ((canon_image (Y,1)) * f)
by FUNCT_1:33;
then A20:
v in dom (((canon_image (Y,1)) * f) * ((canon_image (X,1)) "))
by A19, RELAT_1:27;
then A21:
(free_magmaF f) . v =
(((canon_image (Y,1)) * f) * ((canon_image (X,1)) ")) . v
by A10, PARTFUN1:53
.=
((canon_image (Y,1)) * f) . (((canon_image (X,1)) ") . v)
by A20, FUNCT_1:12
;
x in dom (canon_image (X,1))
by A15, Lm3;
then
((canon_image (X,1)) ") . v = x
by A18, FUNCT_1:34;
hence
w = (free_magmaF f) . v
by A11, A13, A21, FUNCT_1:13;
verum end;
end;
end;
A25:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 4(A3);
A26:
for
w being
Element of
(free_magma Y) ex
v being
Element of
(free_magma X) st
w = (free_magmaF f) . v
ex
x being
set st
(
x in dom (free_magmaF f) &
y = (free_magmaF f) . x )
hence
y in rng (free_magmaF f)
by FUNCT_1:def 3;
verum
end;
then
the carrier of (free_magma Y) c= rng (free_magmaF f)
;
then
rng (free_magmaF f) = the carrier of (free_magma Y)
by XBOOLE_0:def 10;
hence
free_magmaF f is onto
by FUNCT_2:def 3; verum