let f, g be 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
let i, j be Nat; ( 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 implies SUM f = SUM g )
assume that
A1:
f is V115()
and
A2:
i >= j
and
A3:
for n being Nat st n <> i & n <> j holds
f . n = g . n
and
A4:
f . i = g . j
and
A5:
f . j = g . i
; SUM f = SUM g
A6:
SUM f <= SUM g
by A1, A2, A3, A4, A5, Lm13;
for k being Element of NAT holds 0 <= g . k
then
g is V115()
by SUPINF_2:39;
then
SUM g <= SUM f
by A2, A3, A4, A5, Lm13;
hence
SUM f = SUM g
by A6, XXREAL_0:1; verum