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))

A1: ( n + 1 > 0 + 1 & len (Newton_Coeff n) = n + 1 ) by XREAL_1:6, NEWTON:def 5;

A2: Newton_Coeff n = ((Newton_Coeff n) | n) ^ <*((Newton_Coeff n) . (n + 1))*> by NEWTON:def 5, RFINSEQ:7;

A2a: n in dom (Newton_Coeff n) by Th30;

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

then A3: len ((Newton_Coeff n) | n) > 0 by A1, FINSEQ_1:59;

<*((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

A1: ( n + 1 > 0 + 1 & len (Newton_Coeff n) = n + 1 ) by XREAL_1:6, NEWTON:def 5;

A2: Newton_Coeff n = ((Newton_Coeff n) | n) ^ <*((Newton_Coeff n) . (n + 1))*> by NEWTON:def 5, RFINSEQ:7;

A2a: n in dom (Newton_Coeff n) by Th30;

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

then A3: len ((Newton_Coeff n) | n) > 0 by A1, FINSEQ_1:59;

<*((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