let n, k be Element of NAT ; PFBrt n,k is Element of (SubstPoset NAT ,{k})
A1:
for s, t being Element of PFuncs NAT ,{k} st s in PFBrt n,k & t in PFBrt n,k & s c= t holds
s = t
proof
let s,
t be
Element of
PFuncs NAT ,
{k};
( s in PFBrt n,k & t in PFBrt n,k & s c= t implies s = t )
assume that A2:
s in PFBrt n,
k
and A3:
t in PFBrt n,
k
and A4:
s c= t
;
s = t
A5:
( ex
m being non
empty Element of
NAT st
(
m <= n &
s = PFArt m,
k ) or
s = PFCrt n,
k )
by A2, Def4;
A6:
( ex
m being non
empty Element of
NAT st
(
m <= n &
t = PFArt m,
k ) or
t = PFCrt n,
k )
by A3, Def4;
end;
for u being set st u in PFBrt n,k holds
u is finite
by Lm8;
then
( SubstitutionSet NAT ,{k} = the carrier of (SubstPoset NAT ,{k}) & PFBrt n,k in { A where A is Element of Fin (PFuncs NAT ,{k}) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs NAT ,{k} st s in A & t in A & s c= t holds
s = t ) ) } )
by A1, SUBSTLAT:def 4;
hence
PFBrt n,k is Element of (SubstPoset NAT ,{k})
by SUBSTLAT:def 1; verum