let n be Nat; 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; verum