let n be non zero natural number ; :: 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 A: 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 A; :: 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 Element of REAL & max S is Element of NAT & support (ppf n) c= Seg (max S) )
A2: support (ppf n) c= Seg (max S)

proof

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

end;

max S is Element of NAT by ORDINAL1:def 13;
hence ( max S is Element of REAL & max S is Element of NAT & support (ppf n) c= Seg (max S) ) by A2; :: thesis: verum

end;

end;