let k be Element of NAT ; :: thesis: for a being non empty Element of (SubstPoset (NAT,{k}))
for a9 being Element of Fin (PFuncs (NAT,{k})) st a <> {{}} & a = a9 holds
Involved a9 is non empty finite Subset of NAT
let a be non empty Element of (SubstPoset (NAT,{k})); :: thesis: for a9 being Element of Fin (PFuncs (NAT,{k})) st a <> {{}} & a = a9 holds
Involved a9 is non empty finite Subset of NAT
let a9 be Element of Fin (PFuncs (NAT,{k})); :: thesis: ( a <> {{}} & a = a9 implies Involved a9 is non empty finite Subset of NAT )
assume that
A1: a <> {{}} and
A2: a = a9 ; :: thesis: Involved a9 is non empty finite Subset of NAT
consider f being finite Function such that
A3: f in a and
A4: f <> {} by A1, Th33;
ex k1 being object st k1 in dom f by A4, XBOOLE_0:def 1;
hence Involved a9 is non empty finite Subset of NAT by A2, A3, HEYTING2:6, HEYTING2:def 1; :: thesis: verum