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: dom (Ser g) = NAT by FUNCT_2:def 1;
for x being ExtReal st x in rng (Ser f) holds
ex y being ExtReal st
( y in rng (Ser g) & x <= y )

proof

let x be ExtReal; :: thesis: ( x in rng (Ser f) implies ex y being ExtReal st
( y in rng (Ser g) & x <= y ) )
assume x in rng (Ser f) ; :: thesis: ex y being ExtReal st
( y in rng (Ser g) & x <= y )
then consider n being Element of NAT such that
A7: x = (Ser f) . n by FUNCT_2:113;

per cases ( n <= i or n > i ) ;

suppose n <= i ; :: thesis: ex y being ExtReal st
( y in rng (Ser g) & x <= y )

then x <= (Ser f) . i by A1, A7, MEASURE7:8;
then A8: x <= (Ser g) . i by A1, A2, A3, A4, A5, Th49;
i in dom (Ser g) by A6, ORDINAL1:def 12;
hence ex y being ExtReal st
( y in rng (Ser g) & x <= y ) by A8, FUNCT_1:3; :: thesis: verum

end;

suppose A9: n > i ; :: thesis: ex y being ExtReal st
( y in rng (Ser g) & x <= y )

then n >= j by A2, XXREAL_0:2;
then (Ser f) . n = (Ser g) . n by A1, A3, A4, A5, A9, Th50;
hence ex y being ExtReal st
( y in rng (Ser g) & x <= y ) by A6, A7, FUNCT_1:3; :: thesis: verum

end;

end;

end;

hence SUM f <= SUM g by XXREAL_2:63; :: thesis: verum