let X, Y be non empty set ; :: thesis: for f being Function of X,Y holds free_magmaF (id X) = id (dom (free_magmaF f))
let f be Function of X,Y; :: thesis: free_magmaF (id X) = id (dom (free_magmaF f))
dom (free_magmaF (id X)) = the carrier of (free_magma X) by FUNCT_2:def 1;
then A1: dom (free_magmaF (id X)) = dom (free_magmaF f) by FUNCT_2:def 1;
for x being object st x in dom (free_magmaF f) holds
(free_magmaF (id X)) . x = x

proof

let x be object ; :: thesis: ( x in dom (free_magmaF f) implies (free_magmaF (id X)) . x = x )
assume A2: x in dom (free_magmaF f) ; :: thesis: (free_magmaF (id X)) . x = x
defpred S₁[ Nat] means for w being Element of (free_magma X) st length w = $1 holds
(free_magmaF (id X)) . w = w;
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 X) st length w = k holds
(free_magmaF (id X)) . w = w :: thesis: verum

proof

let w be Element of (free_magma X); :: thesis: ( length w = k implies (free_magmaF (id X)) . w = w )
assume A5: length w = k ; :: thesis: (free_magmaF (id X)) . w = w
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 ; :: thesis: (free_magmaF (id X)) . w = w

set y = w `1 ;
w `1 in { (w9 `1) where w9 is Element of (free_magma X) : length w9 = 1 } by A8;
then A9: w `1 in X by Th30;
then A10: w `1 in dom (id X) ;
free_magmaF (id X) extends ((canon_image (X,1)) * (id X)) * ((canon_image (X,1)) ") by Def21;
then A11: ( dom (((canon_image (X,1)) * (id X)) * ((canon_image (X,1)) ")) c= dom (free_magmaF (id X)) & ((canon_image (X,1)) * (id X)) * ((canon_image (X,1)) ") tolerates free_magmaF (id X) ) ;
A12: (canon_image (X,1)) . (w `1) = [(w `1),1] by A9, Lm3
.= w by Def18, A6, A8 ;
A13: w `1 in dom (canon_image (X,1)) by A9, Lm3;
then w in rng (canon_image (X,1)) by A12, FUNCT_1:3;
then A14: w in dom ((canon_image (X,1)) ") by FUNCT_1:33;
rng (id X) = dom (canon_image (X,1)) by Lm3;
then dom ((canon_image (X,1)) * (id X)) = dom (id X) by RELAT_1:27;
then X = dom ((canon_image (X,1)) * (id X)) ;
then dom (canon_image (X,1)) c= dom ((canon_image (X,1)) * (id X)) by Lm3;
then rng ((canon_image (X,1)) ") c= dom ((canon_image (X,1)) * (id X)) by FUNCT_1:33;
then A15: w in dom (((canon_image (X,1)) * (id X)) * ((canon_image (X,1)) ")) by A14, RELAT_1:27;
((canon_image (X,1)) ") . w = w `1 by A13, A12, FUNCT_1:34;
then (((canon_image (X,1)) * (id X)) * ((canon_image (X,1)) ")) . w = ((canon_image (X,1)) * (id X)) . (w `1) by A15, FUNCT_1:12
.= (canon_image (X,1)) . ((id X) . (w `1)) by A10, FUNCT_1:13
.= w by A12, A9, FUNCT_1:18 ;
hence (free_magmaF (id X)) . w = w by A15, A11, PARTFUN1:53; :: thesis: verum

end;

suppose length w >= 2 ; :: thesis: (free_magmaF (id X)) . w = w

then consider w1, w2 being Element of (free_magma X) such that
A16: ( w = w1 * w2 & length w1 < length w & length w2 < length w ) by Th34;
thus (free_magmaF (id X)) . w = ((free_magmaF (id X)) . w1) * ((free_magmaF (id X)) . w2) by A16, GROUP_6:def 6
.= w1 * ((free_magmaF (id X)) . w2) by A4, A5, A16
.= w by A4, A5, A16 ; :: thesis: verum

end;

end;

end;

end;

A17: for k being Nat holds S₁[k] from NAT_1:sch 4(A3);
for w being Element of (free_magma X) holds (free_magmaF (id X)) . w = w

proof

let w be Element of (free_magma X); :: thesis: (free_magmaF (id X)) . w = w
reconsider k = length w as Nat ;
S₁[k] by A17;
hence (free_magmaF (id X)) . w = w ; :: thesis: verum

end;

hence (free_magmaF (id X)) . x = x by A2; :: thesis: verum

end;

hence free_magmaF (id X) = id (dom (free_magmaF f)) by A1, FUNCT_1:17; :: thesis: verum