defpred S₁[ Nat] means n is prime ;
deffunc H₁( set ) -> set = n;
set f = pfexp n;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
set A = { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } ;
A1: support (pfexp n) c= { H₁(i) where i is Nat : ( i <= n & S₁[i] ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (pfexp n) or x in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } )
assume A2: x in support (pfexp n) ; :: thesis: x in { H₁(i) where i is Nat : ( i <= n & S₁[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 { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } ; :: thesis: verum

end;

{ H₁(i) where i is Nat : ( i <= n & S₁[i] ) } is finite from FINSEQ_1:sch 6();
hence support (pfexp n) is finite by A1; :: according to PRE_POLY:def 8 :: thesis: verum