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
zero Element of
NAT st
(
m <= n &
s = PFArt (
m,
k) ) or
s = PFCrt (
n,
k) )
by A2, Def4;
A6:
( ex
m being non
zero 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