let f be real-valued FinSequence; :: thesis: for i, j being Nat
for a, b being Real st i in dom f & j in dom f & i <> j holds
Sum (Replace (f,i,j,a,b)) = ((((Sum f) - (f . i)) - (f . j)) + a) + b
let i, j be Nat; :: thesis: for a, b being Real st i in dom f & j in dom f & i <> j holds
Sum (Replace (f,i,j,a,b)) = ((((Sum f) - (f . i)) - (f . j)) + a) + b
let a, b be Real; :: thesis: ( i in dom f & j in dom f & i <> j implies Sum (Replace (f,i,j,a,b)) = ((((Sum f) - (f . i)) - (f . j)) + a) + b )
assume A0: ( i in dom f & j in dom f & i <> j ) ; :: thesis: Sum (Replace (f,i,j,a,b)) = ((((Sum f) - (f . i)) - (f . j)) + a) + b
A1: j in dom (f +* (i,a)) by A0, FUNCT_7:30;
Sum (Replace (f,i,j,a,b)) = ((Sum (f +* (i,a))) - ((f +* (i,a)) . j)) + b by A1, SumA
.= ((Sum (f +* (i,a))) - (f . j)) + b by FUNCT_7:32, A0
.= ((((Sum f) - (f . i)) + a) - (f . j)) + b by A0, SumA
.= (((Sum f) - (f . i)) + (a - (f . j))) + b ;
hence Sum (Replace (f,i,j,a,b)) = ((((Sum f) - (f . i)) - (f . j)) + a) + b ; :: thesis: verum