let X be non empty set ; :: thesis: for F being Functional_Sequence of X,REAL
for x being Element of X
for n, m being Nat 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,REAL; :: thesis: for x being Element of X
for n, m being Nat 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: for n, m being Nat 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: ( 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 A1: 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 A2: 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 A3: 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 A4: n <= m ; :: thesis: ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x
set PF = Partial_Sums F;
defpred S₁[ Nat] means ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . $1) . x;
A5: 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
A6: (Partial_Sums F) . (k + 1) = ((Partial_Sums F) . k) + (F . (k + 1)) by MESFUN9C:def 2;
A7: dom ((Partial_Sums F) . (k + 1)) = dom (F . 0) by A1, MESFUN9C:11;
( F . (k + 1) is nonnegative & (Partial_Sums F) . k is nonnegative ) by A3, Th67;
then ( 0 <= (F . (k + 1)) . x & 0 <= ((Partial_Sums F) . k) . x ) by MESFUNC6:51;
then (((Partial_Sums F) . k) . x) + 0 <= (((Partial_Sums F) . k) . x) + ((F . (k + 1)) . x) by XREAL_1:7;
hence ((Partial_Sums F) . k) . x <= ((Partial_Sums F) . (k + 1)) . x by A7, A2, A6, VALUED_1:def 1; :: thesis: verum

end;

A8: 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 A9: ( k >= n & ( for l being Nat st l >= n & l < k holds
S₁[l] ) ) ; :: thesis: S₁[k]

now :: thesis: ( k > n implies S₁[k] )

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

now :: thesis: ( k > n + 1 implies S₁[k] )

assume A11: k > n + 1 ; :: thesis: S₁[k]
then reconsider l = k - 1 as Nat by NAT_1:20;
k < k + 1 by NAT_1:13;
then ( k > l & l >= n ) by A11, XREAL_1:19;
then A12: ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . l) . x by A9;
k = l + 1 ;
then ((Partial_Sums F) . l) . x <= ((Partial_Sums F) . k) . x by A5;
hence S₁[k] by A12, XXREAL_0:2; :: thesis: verum

end;

hence S₁[k] by A10, A5; :: thesis: verum

end;

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

end;

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