let n be positive Nat; :: thesis: Sum (Newton_Coeff n) = ((Sum (((Newton_Coeff n) | n) /^ 1)) + ((Newton_Coeff n) . 1)) + ((Newton_Coeff n) . (n + 1))
len (Newton_Coeff n) = n + 1 by NEWTON:def 5;
then A2: Newton_Coeff n = ((Newton_Coeff n) | n) ^ <*((Newton_Coeff n) . (n + 1))*> by RFINSEQ:7;
A2a: n in dom (Newton_Coeff n) by Th30;
A3: len ((Newton_Coeff n) | n) > 0 ;
<*((Newton_Coeff n) . (n + 1))*> is FinSequence of REAL by RVSUM_1:145;
then Sum (Newton_Coeff n) = (Sum ((Newton_Coeff n) | n)) + (Sum <*((Newton_Coeff n) . (n + 1))*>) by Th14, A2
.= (Sum ((Newton_Coeff n) | n)) + ((Newton_Coeff n) . (n + 1)) by RVSUM_1:73
.= ((((Newton_Coeff n) | n) . 1) + (Sum (((Newton_Coeff n) | n) /^ 1))) + ((Newton_Coeff n) . (n + 1)) by A3, IRRAT_1:17 ;
hence Sum (Newton_Coeff n) = ((Sum (((Newton_Coeff n) | n) /^ 1)) + ((Newton_Coeff n) . 1)) + ((Newton_Coeff n) . (n + 1)) by A2a, Th9; :: thesis: verum