let X, Y be non empty set ; :: thesis: for f being Function of X,Y st f is onto holds
free_magmaF f is onto
let f be Function of X,Y; :: thesis: ( f is onto implies free_magmaF f is onto )
assume A1: f is onto ; :: thesis: free_magmaF f is onto
for y being set st y in the carrier of (free_magma Y) holds
y in rng (free_magmaF f)

proof

let y be set ; :: thesis: ( 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) ; :: thesis: y in rng (free_magmaF f)
defpred S₁[ 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
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A4: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[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 :: thesis: verum

proof

let w be Element of (free_magma Y); :: thesis: ( length w = k implies ex v being Element of (free_magma X) st w = (free_magmaF f) . v )
assume A5: length w = k ; :: thesis: 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:10;

per cases ( length w = 1 or length w >= 2 ) by A7, NAT_1:13;

suppose A8: length w = 1 ; :: thesis: ex v being Element of (free_magma X) st w = (free_magmaF f) . v

set 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 Def22;
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 ) by Def3;
A11: (canon_image Y,1) . (w `1 ) = [(w `1 ),1] by A9, Lm2
.= w by Def19, A6, A8 ;
A12: rng f = Y by A1, FUNCT_2:def 3;
then consider x being set such that
A13: ( x in dom f & w `1 = f . x ) by A9, FUNCT_1:def 5;
A14: 1 in {1} by TARSKI:def 1;
A15: x in X by A13;
then x in free_magma X,1 by Def14;
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 ; :: thesis: w = (free_magmaF f) . v
A17: x in dom (canon_image X,1) by Lm2, A15;
A18: v = (canon_image X,1) . x by Lm2, A13;
then v in rng (canon_image X,1) by A17, FUNCT_1:12;
then A19: v in dom ((canon_image X,1) " ) by FUNCT_1:55;
rng f = dom (canon_image Y,1) by Lm2, A12;
then dom f = dom ((canon_image Y,1) * f) by RELAT_1:46;
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 Lm2;
then rng ((canon_image X,1) " ) c= dom ((canon_image Y,1) * f) by FUNCT_1:55;
then A20: v in dom (((canon_image Y,1) * f) * ((canon_image X,1) " )) by A19, RELAT_1:46;
then A21: (free_magmaF f) . v = (((canon_image Y,1) * f) * ((canon_image X,1) " )) . v by A10, PARTFUN1:132
.= ((canon_image Y,1) * f) . (((canon_image X,1) " ) . v) by A20, FUNCT_1:22 ;
x in dom (canon_image X,1) by A15, Lm2;
then ((canon_image X,1) " ) . v = x by A18, FUNCT_1:56;
hence w = (free_magmaF f) . v by A11, A13, A21, FUNCT_1:23; :: thesis: verum

end;

suppose length w >= 2 ; :: thesis: ex v being Element of (free_magma X) st w = (free_magmaF f) . v

then consider w1, w2 being Element of (free_magma Y) such that
A22: ( w = w1 * w2 & length w1 < length w & length w2 < length w ) by Th34;
consider v1 being Element of (free_magma X) such that
A23: w1 = (free_magmaF f) . v1 by A22, A4, A5;
consider v2 being Element of (free_magma X) such that
A24: w2 = (free_magmaF f) . v2 by A22, A4, A5;
take v1 * v2 ; :: thesis: w = (free_magmaF f) . (v1 * v2)
thus w = (free_magmaF f) . (v1 * v2) by A23, A24, A22, GROUP_6:def 7; :: thesis: verum

end;

end;

end;

end;

A26: for k being Nat holds S₁[k] from NAT_1:sch 4(A3);
A27: for w being Element of (free_magma Y) ex v being Element of (free_magma X) st w = (free_magmaF f) . v

proof

let w be Element of (free_magma Y); :: thesis: ex v being Element of (free_magma X) st w = (free_magmaF f) . v
reconsider k = length w as Nat ;
S₁[k] by A26;
hence ex v being Element of (free_magma X) st w = (free_magmaF f) . v ; :: thesis: verum

end;

ex x being set st
( x in dom (free_magmaF f) & y = (free_magmaF f) . x )

proof

consider x being Element of (free_magma X) such that
A28: y = (free_magmaF f) . x by A2, A27;
take x ; :: thesis: ( x in dom (free_magmaF f) & y = (free_magmaF f) . x )
x in the carrier of (free_magma X) ;
hence x in dom (free_magmaF f) by FUNCT_2:def 1; :: thesis: y = (free_magmaF f) . x
thus y = (free_magmaF f) . x by A28; :: thesis: verum

end;

hence y in rng (free_magmaF f) by FUNCT_1:def 5; :: thesis: verum

end;

then the carrier of (free_magma Y) c= rng (free_magmaF f) by TARSKI:def 3;
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; :: thesis: verum