let p be Prime; :: thesis: for n being non zero Nat st n in FreeGen p holds
support (pfexp n) c= Seg p
let n be non zero Nat; :: thesis: ( n in FreeGen p implies support (pfexp n) c= Seg p )
assume n in FreeGen p ; :: thesis: support (pfexp n) c= Seg p
then A2: for i being Prime st i divides n holds
i <= p by FG;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (pfexp n) or x in Seg p )
assume A1: x in support (pfexp n) ; :: thesis: x in Seg p
then reconsider k = x as Prime by NAT_3:34;
A3: 1 < k by INT_2:def 4;
k divides n by A1, NAT_3:36;
hence x in Seg p by A3, FINSEQ_1:1, A2; :: thesis: verum