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
;
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 H1(
object )
-> object =
[$1,n];
A3:
for
x being
object st
x in free_magma (
X,
n) holds
H1(
x)
in the
carrier of
(free_magma X)
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 = H1(
x)
from FUNCT_2:sch 2(A3);
take
f
;
for x being set st x in dom f holds
f . x = [x,n]
let x be
set ;
( x in dom f implies f . x = [x,n] )
assume
x in dom f
;
f . x = [x,n]
hence
f . x = [x,n]
by A6;
verum
end;
A7:
( not n > 0 implies ex f being Function of (free_magma (X,n)),(free_magma X) st f = {} )
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);
( 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
;
( 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]
;
( 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]
;
f1 = f2
end;
hence
( ( for b1 being Function of (free_magma (X,n)),(free_magma X) holds verum ) & ( n > 0 implies ex b1 being Function of (free_magma (X,n)),(free_magma X) st
for x being set st x in dom b1 holds
b1 . x = [x,n] ) & ( not n > 0 implies ex b1 being Function of (free_magma (X,n)),(free_magma X) st b1 = {} ) & ( for b1, b2 being Function of (free_magma (X,n)),(free_magma X) holds
( ( n > 0 & ( for x being set st x in dom b1 holds
b1 . x = [x,n] ) & ( for x being set st x in dom b2 holds
b2 . x = [x,n] ) implies b1 = b2 ) & ( not n > 0 & b1 = {} & b2 = {} implies b1 = b2 ) ) ) )
by A1, A7; verum