let n be Nat; :: thesis: Sum (Newton_Coeff n) = (Sum ((Newton_Coeff n) | n)) + 1

A0: Newton_Coeff n is FinSequence of NAT by Th1;

A1: (Newton_Coeff n) . (n + 1) = ((1,1) In_Power n) . (n + 1) by NEWTON:31

.= 1 ^ n by NEWTON:29 ;

A2: n + 1 = len (Newton_Coeff n) by NEWTON:def 5;

n + 1 >= 0 + 1 by XREAL_1:6;

then A3: n + 1 in dom (Newton_Coeff n) by FINSEQ_3:25, A2;

Newton_Coeff n = ((Newton_Coeff n) | n) ^ <*((Newton_Coeff n) /. (n + 1))*> by A0, A2, FINSEQ_5:21

.= ((Newton_Coeff n) | n) ^ <*((Newton_Coeff n) . (n + 1))*> by A3, PARTFUN1:def 6 ;

hence Sum (Newton_Coeff n) = (Sum ((Newton_Coeff n) | n)) + 1 by A1, RVSUM_1:74; :: thesis: verum

A0: Newton_Coeff n is FinSequence of NAT by Th1;

A1: (Newton_Coeff n) . (n + 1) = ((1,1) In_Power n) . (n + 1) by NEWTON:31

.= 1 ^ n by NEWTON:29 ;

A2: n + 1 = len (Newton_Coeff n) by NEWTON:def 5;

n + 1 >= 0 + 1 by XREAL_1:6;

then A3: n + 1 in dom (Newton_Coeff n) by FINSEQ_3:25, A2;

Newton_Coeff n = ((Newton_Coeff n) | n) ^ <*((Newton_Coeff n) /. (n + 1))*> by A0, A2, FINSEQ_5:21

.= ((Newton_Coeff n) | n) ^ <*((Newton_Coeff n) . (n + 1))*> by A3, PARTFUN1:def 6 ;

hence Sum (Newton_Coeff n) = (Sum ((Newton_Coeff n) | n)) + 1 by A1, RVSUM_1:74; :: thesis: verum