A1: ( n > 0 implies ex f being Function of (free_magma (X,n)),(free_magma X) st
for x being set st x in dom f holds
f . x = [x,n] )

proof

assume A2: n > 0 ; :: thesis: ex f being Function of (free_magma (X,n)),(free_magma X) st
for x being set st x in dom f holds
f . x = [x,n]
deffunc H₁( object ) -> object = [$1,n];
A3: for x being object st x in free_magma (X,n) holds
H₁(x) in the carrier of (free_magma X)

proof

let x be object ; :: thesis: ( x in free_magma (X,n) implies H₁(x) in the carrier of (free_magma X) )
assume A4: x in free_magma (X,n) ; :: thesis: H₁(x) in the carrier of (free_magma X)
n in {n} by TARSKI:def 1;
then A5: H₁(x) in [:(free_magma (X,n)),{n}:] by A4, ZFMISC_1:def 2;
[:(free_magma (X,n)),{n}:] c= free_magma_carrier X by A2, Lm1;
hence H₁(x) in the carrier of (free_magma X) by A5; :: thesis: verum

end;

consider f being Function of (free_magma (X,n)), the carrier of (free_magma X) such that
A6: for x being object st x in free_magma (X,n) holds
f . x = H₁(x) from FUNCT_2:sch 2(A3);
take f ; :: thesis: for x being set st x in dom f holds
f . x = [x,n]
let x be set ; :: thesis: ( x in dom f implies f . x = [x,n] )
assume x in dom f ; :: thesis: f . x = [x,n]
hence f . x = [x,n] by A6; :: thesis: verum

end;

A7: ( not n > 0 implies ex f being Function of (free_magma (X,n)),(free_magma X) st f = {} )

proof

assume not n > 0 ; :: thesis: ex f being Function of (free_magma (X,n)),(free_magma X) st f = {}
then n = 0 ;
then A8: free_magma (X,n) = {} by Def13;
set f = {} ;
A9: dom {} = {} ;
rng {} c= the carrier of (free_magma X) ;
then reconsider f = {} as Function of (free_magma (X,n)),(free_magma X) by A8, A9, FUNCT_2:2;
take f ; :: thesis: f = {}
thus f = {} ; :: thesis: verum

end;

for f1, f2 being Function of (free_magma (X,n)),(free_magma X) st n > 0 & ( for x being set st x in dom f1 holds
f1 . x = [x,n] ) & ( for x being set st x in dom f2 holds
f2 . x = [x,n] ) holds
f1 = f2

proof

let f1, f2 be Function of (free_magma (X,n)),(free_magma X); :: thesis: ( n > 0 & ( for x being set st x in dom f1 holds
f1 . x = [x,n] ) & ( for x being set st x in dom f2 holds
f2 . x = [x,n] ) implies f1 = f2 )
assume n > 0 ; :: thesis: ( ex x being set st
( x in dom f1 & not f1 . x = [x,n] ) or ex x being set st
( x in dom f2 & not f2 . x = [x,n] ) or f1 = f2 )
assume A10: for x being set st x in dom f1 holds
f1 . x = [x,n] ; :: thesis: ( ex x being set st
( x in dom f2 & not f2 . x = [x,n] ) or f1 = f2 )
assume A11: for x being set st x in dom f2 holds
f2 . x = [x,n] ; :: thesis: f1 = f2

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: f1 = f2

hence f1 = f2 ; :: thesis: verum

end;

suppose A12: not X is empty ; :: thesis: f1 = f2

then A13: dom f1 = free_magma (X,n) by FUNCT_2:def 1
.= dom f2 by A12, FUNCT_2:def 1 ;
for x being object st x in dom f1 holds
f1 . x = f2 . x

proof

let x be object ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume A14: x in dom f1 ; :: thesis: f1 . x = f2 . x
hence f1 . x = [x,n] by A10
.= f2 . x by A11, A13, A14 ;
:: thesis: verum

end;

hence f1 = f2 by A13, FUNCT_1:2; :: thesis: verum

end;

end;

end;

hence ( ( for b₁ being Function of (free_magma (X,n)),(free_magma X) holds verum ) & ( n > 0 implies ex b₁ being Function of (free_magma (X,n)),(free_magma X) st
for x being set st x in dom b₁ holds
b₁ . x = [x,n] ) & ( not n > 0 implies ex b₁ being Function of (free_magma (X,n)),(free_magma X) st b₁ = {} ) & ( for b₁, b₂ being Function of (free_magma (X,n)),(free_magma X) holds
( ( n > 0 & ( for x being set st x in dom b₁ holds
b₁ . x = [x,n] ) & ( for x being set st x in dom b₂ holds
b₂ . x = [x,n] ) implies b₁ = b₂ ) & ( not n > 0 & b₁ = {} & b₂ = {} implies b₁ = b₂ ) ) ) ) by A1, A7; :: thesis: verum