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, Th36;
ex k1 being set 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:10, HEYTING2:12, HEYTING2:def 1; :: thesis: verum