defpred S1[ Nat] means n is prime ;
deffunc H1( set ) -> set = n;
set f = pfexp n;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
set A = { H1(i) where i is Nat : ( i <= n & S1[i] ) } ;
A1: support (pfexp n) c= { H1(i) where i is Nat : ( i <= n & S1[i] ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (pfexp n) or x in { H1(i) where i is Nat : ( i <= n & S1[i] ) } )
assume A2: x in support (pfexp n) ; :: thesis: x in { H1(i) where i is Nat : ( i <= n & S1[i] ) }
then reconsider x = x as Prime by Th34;
(pfexp n) . x <> 0 by A2, PRE_POLY:def 7;
then ( x is prime Element of NAT & x <= n ) by Th35, ORDINAL1:def 12;
hence x in { H1(i) where i is Nat : ( i <= n & S1[i] ) } ; :: thesis: verum
end;
{ H1(i) where i is Nat : ( i <= n & S1[i] ) } is finite from FINSEQ_1:sch 6();
 hence support (pfexp n) is finite by A1; :: according to PRE_POLY:def 8 :: thesis: verum