let p be Prime; :: thesis: for n being non zero Nat st n in FreeGen p holds
card (support (pfexp n)) <= p
let n be non zero Nat; :: thesis: ( n in FreeGen p implies card (support (pfexp n)) <= p )
assume n in FreeGen p ; :: thesis: card (support (pfexp n)) <= p
then card (support (pfexp n)) <= card (Seg p) by NAT_1:43, Lm1;
hence card (support (pfexp n)) <= p by FINSEQ_1:57; :: thesis: verum