let f, g be sequence of ExtREAL; :: thesis: 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; :: thesis: ( 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 ; :: 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