let f, g be sequence of ExtREAL; :: thesis: ( f is nonnegative & ex N being Nat st
( (Ser f) . N <= (Ser g) . N & ( for n being Nat st n > N holds
f . n <= g . n ) ) implies SUM f <= SUM g )
assume that
A1: f is nonnegative and
A2: ex N being Nat st
( (Ser f) . N <= (Ser g) . N & ( for n being Nat st n > N holds
f . n <= g . n ) ) ; :: thesis: SUM f <= SUM g
consider N being Nat such that
A3: (Ser f) . N <= (Ser g) . N and
A4: for n being Nat st n > N holds
f . n <= g . n by A2;
defpred S₁[ Nat] means (Ser f) . (N + $1) <= (Ser g) . (N + $1);
A5: S₁[ 0 ] by A3;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
A8: ( (Ser f) . ((N + k) + 1) = ((Ser f) . (N + k)) + (f . ((N + k) + 1)) & (Ser g) . ((N + k) + 1) = ((Ser g) . (N + k)) + (g . ((N + k) + 1)) ) by SUPINF_2:def 11;
N < (N + k) + 1 by NAT_1:11, NAT_1:13;
then f . ((N + k) + 1) <= g . ((N + k) + 1) by A4;
hence S₁[k + 1] by A7, A8, XXREAL_3:36; :: thesis: verum

end;

A9: for m being Nat holds S₁[m] from NAT_1:sch 2(A5, A6);
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
A10: x = (Ser f) . n by FUNCT_2:113;

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

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

then reconsider m = N - n as Nat by NAT_1:21;
N = n + m ;
then (Ser f) . n <= (Ser f) . N by A1, SUPINF_2:41;
then A11: x <= (Ser g) . N by A3, A10, XXREAL_0:2;
dom (Ser g) = NAT by FUNCT_2:def 1;
then N in dom (Ser g) by ORDINAL1:def 12;
hence ex y being ExtReal st
( y in rng (Ser g) & x <= y ) by A11, FUNCT_1:3; :: thesis: verum

end;

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

then reconsider m = n - N as Nat by NAT_1:21;
A12: x <= (Ser g) . (N + m) by A9, A10;
dom (Ser g) = NAT by FUNCT_2:def 1;
hence ex y being ExtReal st
( y in rng (Ser g) & x <= y ) by A12, FUNCT_1:3; :: thesis: verum

end;

end;

end;

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