let f, g be sequence of ExtREAL; :: thesis: 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
let i, j be Nat; :: thesis: ( 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 implies SUM f = SUM g )
assume that
A1: f is nonnegative 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 ; :: thesis: 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

proof

let k be Element of NAT ; :: thesis: 0 <= g . k

per cases ( k = i or k = j or ( k <> i & k <> j ) ) ;

suppose ( k = i or k = j ) ; :: thesis: 0 <= g . k

hence 0 <= g . k by A1, A4, A5, SUPINF_2:51; :: thesis: verum

end;

suppose ( k <> i & k <> j ) ; :: thesis: 0 <= g . k

then g . k = f . k by A3;
hence 0 <= g . k by A1, SUPINF_2:51; :: thesis: verum

end;

end;

end;

then g is nonnegative 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; :: thesis: verum