take
n + 1
; :: according to ALGSEQ_1:def 1 :: thesis: for b_{1} being set holds

( not n + 1 <= b_{1} or (npoly (R,n)) . b_{1} = 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

( not n + 1 <= b

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