set f = Newton_Coeff n;
0 in REAL by XREAL_0:def 1;
then reconsider g = n |-> 0 as FinSequence of REAL by FINSEQ_2:63;
A1: for x being Nat holds (Newton_Coeff n) . x >= (n |-> 0) . x ;
(Newton_Coeff n) . (0 + 1) > g . (0 + 1) ;
then Sum (Newton_Coeff n) > Sum (n |-> 0) by A1, NYS1;
hence not Sum (Newton_Coeff n) is zero ; :: thesis: verum