let k be Element of NAT ; :: thesis: for a being Element of (SubstPoset NAT ,{k})
for a' being Element of Fin (PFuncs NAT ,{k})
for B being non empty finite Subset of NAT st B = Involved a' & a' = a holds
for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X
let a be Element of (SubstPoset NAT ,{k}); :: thesis: for a' being Element of Fin (PFuncs NAT ,{k})
for B being non empty finite Subset of NAT st B = Involved a' & a' = a holds
for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X
let a' be Element of Fin (PFuncs NAT ,{k}); :: thesis: for B being non empty finite Subset of NAT st B = Involved a' & a' = a holds
for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X
let B be non empty finite Subset of NAT ; :: thesis: ( B = Involved a' & a' = a implies for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X )
assume A1: ( B = Involved a' & a' = a ) ; :: thesis: for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X
let X be set ; :: thesis: ( X in a implies for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X )
assume A2: X in a ; :: thesis: for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X
let l be Element of NAT ; :: thesis: ( l > (max B) + 1 implies not [l,k] in X )
assume A3: l > (max B) + 1 ; :: thesis: not [l,k] in X
assume A4: [l,k] in X ; :: thesis: contradiction
SubstitutionSet NAT ,{k} = the carrier of (SubstPoset NAT ,{k}) by SUBSTLAT:def 4;
then reconsider X' = X as finite Function by A2, HEYTING2:2;
A5: (max B) + 1 >= max B by NAT_1:11;
l in dom X' by A4, RELAT_1:def 4;
then l in Involved a' by A1, A2, HEYTING2:def 1;
then max B >= l by A1, XXREAL_2:def 8;
hence contradiction by A3, A5, XXREAL_0:2; :: thesis: verum