let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for x being Element of X st F is with_the_same_dom & x in dom (F . 0 ) & ( for k being Nat holds F . k is nonnegative ) & n <= m holds
((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x
let F be Functional_Sequence of X,ExtREAL ; :: thesis: for n, m being Nat
for x being Element of X st F is with_the_same_dom & x in dom (F . 0 ) & ( for k being Nat holds F . k is nonnegative ) & n <= m holds
((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x
let n, m be Nat; :: thesis: for x being Element of X st F is with_the_same_dom & x in dom (F . 0 ) & ( for k being Nat holds F . k is nonnegative ) & n <= m holds
((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x
let x be Element of X; :: thesis: ( F is with_the_same_dom & x in dom (F . 0 ) & ( for k being Nat holds F . k is nonnegative ) & n <= m implies ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x )
assume A0: F is with_the_same_dom ; :: thesis: ( not x in dom (F . 0 ) or ex k being Nat st not F . k is nonnegative or not n <= m or ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x )
assume A81: x in dom (F . 0 ) ; :: thesis: ( ex k being Nat st not F . k is nonnegative or not n <= m or ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x )
assume A1: for m being Nat holds F . m is nonnegative ; :: thesis: ( not n <= m or ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x )
assume C1: n <= m ; :: thesis: ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x
A2: F is additive by A1, LIM4;
set PF = Partial_Sums F;
defpred S₁[ Nat] means ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . $1) . x;
Q1: for k being Nat holds ((Partial_Sums F) . k) . x <= ((Partial_Sums F) . (k + 1)) . x

proof

let k be Nat; :: thesis: ((Partial_Sums F) . k) . x <= ((Partial_Sums F) . (k + 1)) . x
Q11: (Partial_Sums F) . (k + 1) = ((Partial_Sums F) . k) + (F . (k + 1)) by Def0;
dom ((Partial_Sums F) . (k + 1)) = dom (F . 0 ) by A0, A2, ADD0;
then Q12: ((Partial_Sums F) . (k + 1)) . x = (((Partial_Sums F) . k) . x) + ((F . (k + 1)) . x) by A81, Q11, MESFUNC1:def 3;
( F . (k + 1) is nonnegative & (Partial_Sums F) . k is nonnegative ) by A1, ADD3C;
then ( 0. <= (F . (k + 1)) . x & 0. <= ((Partial_Sums F) . k) . x ) by SUPINF_2:58;
hence ((Partial_Sums F) . k) . x <= ((Partial_Sums F) . (k + 1)) . x by Q12, XXREAL_3:42; :: thesis: verum

end;

Q2: for k being Nat st k >= n & ( for l being Nat st l >= n & l < k holds
S₁[l] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( k >= n & ( for l being Nat st l >= n & l < k holds
S₁[l] ) implies S₁[k] )
assume Q21: ( k >= n & ( for l being Nat st l >= n & l < k holds
S₁[l] ) ) ; :: thesis: S₁[k]

now

assume k > n ; :: thesis: S₁[k]
then k >= n + 1 by NAT_1:13;
then Q22: ( k = n + 1 or k > n + 1 ) by XXREAL_0:1;

now

assume Q23: k > n + 1 ; :: thesis: S₁[k]
then reconsider l = k - 1 as Element of NAT by NAT_1:20;
k < k + 1 by NAT_1:13;
then ( k > l & l >= n ) by Q23, XREAL_1:21;
then Q24: ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . l) . x by Q21;
k = l + 1 ;
then ((Partial_Sums F) . l) . x <= ((Partial_Sums F) . k) . x by Q1;
hence S₁[k] by Q24, XXREAL_0:2; :: thesis: verum

end;

hence S₁[k] by Q22, Q1; :: thesis: verum

end;

hence S₁[k] by Q21, XXREAL_0:1; :: thesis: verum

end;

for k being Nat st k >= n holds
S₁[k] from NAT_1:sch 9(Q2);
hence ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x by C1; :: thesis: verum