consider n being Nat such that
A1: for i being Nat st i >= n holds
p . i = 0. F_Real by ALGSEQ_1:def 1;
take n ; :: according to ALGSEQ_1:def 1 :: thesis: for b₁ being set holds
( not n <= b₁ or (poly_diff p) . b₁ = 0. F_Real )
let i be Nat; :: thesis: ( not n <= i or (poly_diff p) . i = 0. F_Real )
assume A2: i >= n ; :: thesis: (poly_diff p) . i = 0. F_Real
i + 1 >= i + 0 by XREAL_1:6;
then p . (i + 1) = 0. F_Real by A1, A2, XXREAL_0:2;
hence 0. F_Real = (p . (i + 1)) * (i + 1)
.= (poly_diff p) . i by Def5 ;
:: thesis: verum