let X, Y be non empty set ; for f being Function of X,Y holds free_magmaF (id X) = id (dom (free_magmaF f))
let f be Function of X,Y; 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 ;
( x in dom (free_magmaF f) implies (free_magmaF (id X)) . x = x )
assume A2:
x in dom (free_magmaF f)
;
(free_magmaF (id X)) . x = x
defpred S1[
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
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 X) st
length w = k holds
(free_magmaF (id X)) . w = w
verumproof
let w be
Element of
(free_magma X);
( length w = k implies (free_magmaF (id X)) . w = w )
assume A5:
length w = k
;
(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
;
(free_magmaF (id X)) . w = wset 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) =
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;
verum end; end;
end;
end;
A17:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 4(A3);
for
w being
Element of
(free_magma X) holds
(free_magmaF (id X)) . w = w
hence
(free_magmaF (id X)) . x = x
by A2;
verum
end;
hence
free_magmaF (id X) = id (dom (free_magmaF f))
by A1, FUNCT_1:17; verum