let F1, F2 be sequence of ExtREAL; :: thesis: ( ( for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ) implies SUM F1 <= SUM F2 )

assume A1: for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ; :: thesis: SUM F1 <= SUM F2

A2: for x being ExtReal st x in rng (Ser F1) holds

ex y being ExtReal st

( y in rng (Ser F2) & x <= y )

hence SUM F1 <= SUM F2 by A2, XXREAL_2:63; :: thesis: verum

assume A1: for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ; :: thesis: SUM F1 <= SUM F2

A2: for x being ExtReal st x in rng (Ser F1) holds

ex y being ExtReal st

( y in rng (Ser F2) & x <= y )

proof

( SUM F1 = sup (rng (Ser F1)) & SUM F2 = sup (rng (Ser F2)) )
by SUPINF_2:def 13;
let x be ExtReal; :: thesis: ( x in rng (Ser F1) implies ex y being ExtReal st

( y in rng (Ser F2) & x <= y ) )

A3: dom (Ser F1) = NAT by FUNCT_2:def 1;

assume x in rng (Ser F1) ; :: thesis: ex y being ExtReal st

( y in rng (Ser F2) & x <= y )

then consider n being object such that

A4: n in NAT and

A5: x = (Ser F1) . n by A3, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A4;

reconsider y = (Ser F2) . n as R_eal ;

take y ; :: thesis: ( y in rng (Ser F2) & x <= y )

dom (Ser F2) = NAT by FUNCT_2:def 1;

hence ( y in rng (Ser F2) & x <= y ) by A1, A5, FUNCT_1:def 3; :: thesis: verum

end;( y in rng (Ser F2) & x <= y ) )

A3: dom (Ser F1) = NAT by FUNCT_2:def 1;

assume x in rng (Ser F1) ; :: thesis: ex y being ExtReal st

( y in rng (Ser F2) & x <= y )

then consider n being object such that

A4: n in NAT and

A5: x = (Ser F1) . n by A3, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A4;

reconsider y = (Ser F2) . n as R_eal ;

take y ; :: thesis: ( y in rng (Ser F2) & x <= y )

dom (Ser F2) = NAT by FUNCT_2:def 1;

hence ( y in rng (Ser F2) & x <= y ) by A1, A5, FUNCT_1:def 3; :: thesis: verum

hence SUM F1 <= SUM F2 by A2, XXREAL_2:63; :: thesis: verum