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 & f <> {} ) by A1, Th36;
dom f <> {} by A3;
then consider k1 being set such that
A4: k1 in dom f by XBOOLE_0:def 1;
thus Involved a' is non empty finite Subset of NAT by A2, A3, A4, HEYTING2:10, HEYTING2:12, HEYTING2:def 1; :: thesis: verum