let f be FinSequence of REAL ; :: thesis: for n being positive Nat st n + 1 = len f holds
Sum f = ((Sum ((f | n) /^ 1)) + (f . 1)) + (f . (n + 1))
let n be positive Nat; :: thesis: ( n + 1 = len f implies Sum f = ((Sum ((f | n) /^ 1)) + (f . 1)) + (f . (n + 1)) )
assume A0: n + 1 = len f ; :: thesis: Sum f = ((Sum ((f | n) /^ 1)) + (f . 1)) + (f . (n + 1))
A2: f = (f | n) ^ <*(f . (n + 1))*> by A0, RFINSEQ:7;
( n >= 1 & len f >= n ) by A0, NAT_1:13, NAT_1:14;
then A2a: n in dom f by FINSEQ_3:25;
n + 1 > n + 0 by XREAL_1:6;
then A3: len (f | n) > 0 by A0, FINSEQ_1:59;
<*(f . (n + 1))*> is FinSequence of REAL by RVSUM_1:145;
then Sum f = (Sum (f | n)) + (Sum <*(f . (n + 1))*>) by Th14, A2
.= (Sum (f | n)) + (f . (n + 1)) by RVSUM_1:73
.= (((f | n) . 1) + (Sum ((f | n) /^ 1))) + (f . (n + 1)) by A3, IRRAT_1:17 ;
hence Sum f = ((Sum ((f | n) /^ 1)) + (f . 1)) + (f . (n + 1)) by A2a, Th9; :: thesis: verum