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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support (p removed_last) or x in { H₁(w) where w is Element of Bags (n + 1) : w in Support p } )
assume A3: x in Support (p removed_last) ; :: thesis: x in { H₁(w) where w is Element of Bags (n + 1) : w in Support p }
then reconsider b = x as bag of n ;
A4: ( b bag_extend 0 in Bags (n + 1) & Bags (n + 1) = dom p ) by PARTFUN1:def 2;
(p removed_last) . b <> 0. L by A3, POLYNOM1:def 3;
then p . (b bag_extend 0) <> 0. L by Def6;
then A5: b bag_extend 0 in Support p by A4, POLYNOM1:def 3;
(0,n) -cut (b bag_extend 0) = b by HILB10_2:5;
then H₁(b bag_extend 0) = b by NAT_1:11, HILB10_2:3;
hence x in { H₁(w) where w is Element of Bags (n + 1) : w in Support p } by A5; :: thesis: verum

end;

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