theorem Th51: :: MEASUR12:51

for f, g being sequence of ExtREAL
for i, j being Nat st f is nonnegative & 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