let f be real-valued FinSequence; :: thesis: for i being Nat
for a being Real st i in dom f holds
Sum (f +* (i,a)) = ((Sum f) - (f . i)) + a
let i be Nat; :: thesis: for a being Real st i in dom f holds
Sum (f +* (i,a)) = ((Sum f) - (f . i)) + a
let a be Real; :: thesis: ( i in dom f implies Sum (f +* (i,a)) = ((Sum f) - (f . i)) + a )
reconsider w = f as FinSequence of REAL by RVSUM_1:145;
reconsider aa = a as Element of REAL by XREAL_0:def 1;
assume A1: i in dom f ; :: thesis: Sum (f +* (i,a)) = ((Sum f) - (f . i)) + a
then Z1: Sum (w +* (i,a)) = Sum (((w | (i -' 1)) ^ <*aa*>) ^ (w /^ i)) by CopyForValued
.= (Sum ((w | (i -' 1)) ^ <*aa*>)) + (Sum (w /^ i)) by RVSUM_1:75
.= ((Sum (w | (i -' 1))) + (Sum <*aa*>)) + (Sum (w /^ i)) by RVSUM_1:75
.= ((Sum (w | (i -' 1))) + aa) + (Sum (w /^ i)) by RVSUM_1:73
.= aa + ((Sum (w | (i -' 1))) + (Sum (w /^ i)))
.= aa + (Sum ((w | (i -' 1)) ^ (w /^ i))) by RVSUM_1:75 ;
reconsider fi = f . i as Real ;
( 1 <= i & i <= len w ) by A1, FINSEQ_3:25;
then Sum w = Sum (((w | (i -' 1)) ^ <*(f . i)*>) ^ (w /^ i)) by FINSEQ_5:84
.= (Sum ((w | (i -' 1)) ^ <*(f . i)*>)) + (Sum (w /^ i)) by RVSUM_1:75
.= ((Sum (w | (i -' 1))) + (Sum <*(f . i)*>)) + (Sum (w /^ i)) by RVSUM_1:75
.= ((Sum (w | (i -' 1))) + fi) + (Sum (w /^ i)) by RVSUM_1:73
.= fi + ((Sum (w | (i -' 1))) + (Sum (w /^ i)))
.= fi + (Sum ((w | (i -' 1)) ^ (w /^ i))) by RVSUM_1:75 ;
hence Sum (f +* (i,a)) = ((Sum f) - (f . i)) + a by Z1; :: thesis: verum