let F1, F2 be Function of NAT , 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: SUM F1 = sup (rng (Ser F1)) by SUPINF_2:def 23;
A3: SUM F2 = sup (rng (Ser F2)) by SUPINF_2:def 23;
for x being ext-real number st x in rng (Ser F1) holds
ex y being ext-real number st
( y in rng (Ser F2) & x <= y )

proof

let x be ext-real number ; :: thesis: ( x in rng (Ser F1) implies ex y being ext-real number st
( y in rng (Ser F2) & x <= y ) )
assume A4: x in rng (Ser F1) ; :: thesis: ex y being ext-real number st
( y in rng (Ser F2) & x <= y )
A5: ( dom (Ser F1) = NAT & dom (Ser F2) = NAT & rng (Ser F2) c= ExtREAL ) by FUNCT_2:def 1;
then consider n being set such that
A6: ( n in NAT & x = (Ser F1) . n ) by A4, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A6;
reconsider y = (Ser F2) . n as R_eal ;
take y ; :: thesis: ( y in rng (Ser F2) & x <= y )
thus ( y in rng (Ser F2) & x <= y ) by A1, A5, A6, FUNCT_1:def 5; :: thesis: verum

end;

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