let n be non zero Nat; :: thesis:
A1: support (ppf n) = support (pfexp n) by NAT_3:def 9;

suppose A2: support (ppf n) is empty ; :: thesis:

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

end;

suppose not support (ppf n) is empty ; :: thesis:

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A4: x in support (ppf n) ; :: thesis:
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:

end;

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

end;

end;