take n + 1 ; :: according to ALGSEQ_1:def 1 :: thesis: for b₁ being set holds
( not n + 1 <= b₁ or (npoly (R,n)) . b₁ = 0. R )
let i be Nat; :: thesis: ( not n + 1 <= i or (npoly (R,n)) . i = 0. R )
assume i >= n + 1 ; :: thesis: (npoly (R,n)) . i = 0. R
then i > n by NAT_1:13;
hence (npoly (R,n)) . i = 0. R by Lm11; :: thesis: verum