( Support p = Support |.p.| & Support p is finite ) by Lm18, POLYNOM1:def 5;
hence for b₁ being the carrier of INT.Ring -valued Function st b₁ = |.p.| holds
b₁ is finite-Support by POLYNOM1:def 5; :: thesis: verum