for f, g being sequence of ExtREAL
for i, j being Nat st f is V115() & i >= j & ( for n being Nat st n <> i & n <> j holds
f . n = g . n ) & f . i = g . j & f . j = g . i holds
SUM f = SUM g