let i be Nat; :: thesis: for f being FinSequence of NAT st i in dom f holds
Sum (f | i) = (Sum (f | (i -' 1))) + (f . i)
let f be FinSequence of NAT ; :: thesis: ( i in dom f implies Sum (f | i) = (Sum (f | (i -' 1))) + (f . i) )
set g = <*(f /. i)*>;
set h = f | (i -' 1);
assume A1: i in dom f ; :: thesis: Sum (f | i) = (Sum (f | (i -' 1))) + (f . i)
then i >= 1 by FINSEQ_3:25;
then i -' 1 = i - 1 by XREAL_1:233;
then A2: i = (i -' 1) + 1 ;
A3: f /. i = f . i by A1, PARTFUN1:def 6;
hence (Sum (f | (i -' 1))) + (f . i) = Sum ((f | (i -' 1)) ^ <*(f /. i)*>) by RVSUM_1:74
.= Sum (f | i) by A1, A2, A3, FINSEQ_5:10 ;
:: thesis: verum