deffunc H₁( Element of Bags X) -> Element of K16(X) = support X;
A1: Support p is finite by POLYNOM1:def 5;
set Y = { H₁(b) where b is Element of Bags X : b in Support p } ;
A2: { H₁(b) where b is Element of Bags X : b in Support p } is finite from FRAENKEL:sch 21(A1);
for A being set st A in { H₁(b) where b is Element of Bags X : b in Support p } holds
A is finite

proof

let A be set ; :: thesis: ( A in { H₁(b) where b is Element of Bags X : b in Support p } implies A is finite )
assume A in { H₁(b) where b is Element of Bags X : b in Support p } ; :: thesis: A is finite
then ex b being Element of Bags X st
( A = H₁(b) & b in Support p ) ;
hence A is finite ; :: thesis: verum

end;

then union { H₁(b) where b is Element of Bags X : b in Support p } is finite by A2, FINSET_1:7;
hence vars p is finite by Th39; :: thesis: verum