let k be Element of NAT ; :: thesis: for a being non empty Element of (SubstPoset NAT ,{k})
for a' being Element of Fin (PFuncs NAT ,{k}) st a <> {{} } & a = a' holds
Involved a' is non empty finite Subset of NAT
let a be non empty Element of (SubstPoset NAT ,{k}); :: thesis: for a' being Element of Fin (PFuncs NAT ,{k}) st a <> {{} } & a = a' holds
Involved a' is non empty finite Subset of NAT
let a' be Element of Fin (PFuncs NAT ,{k}); :: thesis: ( a <> {{} } & a = a' implies Involved a' is non empty finite Subset of NAT )
assume that
A1: a <> {{} } and
A2: a = a' ; :: thesis: Involved a' 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 a' is non empty finite Subset of NAT by A2, A3, HEYTING2:10, HEYTING2:12, HEYTING2:def 1; :: thesis: verum