deffunc H₁( bag of n) -> Element of Bags (n + 1) = n bag_extend 0;
A1: Support p is finite by POLYNOM1:def 5;
set FS = { H₁(w) where w is Element of Bags n : w in Support p } ;
A2: { H₁(w) where w is Element of Bags n : w in Support p } is finite from FRAENKEL:sch 21(A1);
set P = p extended_by_0 ;
Support (p extended_by_0) c= { H₁(w) where w is Element of Bags n : w in Support p }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support (p extended_by_0) or x in { H₁(w) where w is Element of Bags n : w in Support p } )
assume A3: x in Support (p extended_by_0) ; :: thesis: x in { H₁(w) where w is Element of Bags n : w in Support p }
then reconsider b = x as bag of n + 1 ;
A4: n -' 0 = n by NAT_D:40;
then reconsider B = (0,n) -cut b as bag of n ;
A5: b . n = 0 by A3, Th7;
then B in Support p by A3, Th9;
then H₁(B) in { H₁(w) where w is Element of Bags n : w in Support p } ;
hence x in { H₁(w) where w is Element of Bags n : w in Support p } by A4, A5, Th4; :: thesis: verum

end;

hence p extended_by_0 is finite-Support by A2, POLYNOM1:def 5; :: thesis: verum