let n be non zero Nat; :: thesis: ex k being Element of NAT st support (ppf n) c= Seg k
A1: support (ppf n) = support (pfexp n) by NAT_3:def 9;

per cases ( support (ppf n) is empty or not support (ppf n) is empty ) ;

suppose A2: support (ppf n) is empty ; :: thesis: ex k being Element of NAT st support (ppf n) c= Seg k

take 0 ; :: thesis: support (ppf n) c= Seg 0
thus support (ppf n) c= Seg 0 by A2; :: thesis: verum

end;

suppose not support (ppf n) is empty ; :: thesis: ex k being Element of NAT st support (ppf n) c= Seg k

then reconsider S = support (ppf n) as non empty finite Subset of NAT by XBOOLE_1:1;
take max S ; :: thesis: ( max S is set & max S is Element of NAT & support (ppf n) c= Seg (max S) )
A3: max S is Element of NAT by ORDINAL1:def 12;
support (ppf n) c= Seg (max S)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf n) or x in Seg (max S) )
assume A4: x in support (ppf n) ; :: thesis: x in Seg (max S)
then reconsider m = x as Nat ;
x is Prime by A1, A4, NAT_3:34;
then A5: 1 <= m by INT_2:def 4;
m <= max S by A4, XXREAL_2:def 8;
hence x in Seg (max S) by A5, FINSEQ_1:1; :: thesis: verum

end;

hence ( max S is set & max S is Element of NAT & support (ppf n) c= Seg (max S) ) by A3; :: thesis: verum

end;

end;