let n, k be Element of NAT ; :: thesis: PFBrt n,k is Element of (SubstPoset NAT ,{k})
A1:
for u being set st u in PFBrt n,k holds
u is finite
by Lm8;
A2:
SubstitutionSet NAT ,{k} = the carrier of (SubstPoset NAT ,{k})
by SUBSTLAT:def 4;
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};
:: thesis: ( s in PFBrt n,k & t in PFBrt n,k & s c= t implies s = t )
assume A3:
(
s in PFBrt n,
k &
t in PFBrt n,
k &
s c= t )
;
:: thesis: s = t
then A4:
( ex
m being non
empty Element of
NAT st
(
m <= n &
s = PFArt m,
k ) or
s = PFCrt n,
k )
by Def4;
A5:
( ex
m being non
empty Element of
NAT st
(
m <= n &
t = PFArt m,
k ) or
t = PFCrt n,
k )
by A3, Def4;
end;
then
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;
hence
PFBrt n,k is Element of (SubstPoset NAT ,{k})
by A2, SUBSTLAT:def 1; :: thesis: verum