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