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 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 )
set PF = Partial_Sums F;
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 )
defpred S₁[ Nat] means ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . $1) . 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 )
A4: 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
A5: (Partial_Sums F) . (k + 1) = ((Partial_Sums F) . k) + (F . (k + 1)) by Def4;
F . (k + 1) is nonnegative by A3;
then A6: 0. <= (F . (k + 1)) . x by SUPINF_2:39;
dom ((Partial_Sums F) . (k + 1)) = dom (F . 0) by A1, A3, Th29, Th30;
then ((Partial_Sums F) . (k + 1)) . x = (((Partial_Sums F) . k) . x) + ((F . (k + 1)) . x) by A2, A5, MESFUNC1:def 3;
hence ((Partial_Sums F) . k) . x <= ((Partial_Sums F) . (k + 1)) . x by A6, XXREAL_3:39; :: thesis: verum

end;

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

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

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

assume A11: 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 A12: k > l by XREAL_1:19;
k = l + 1 ;
then A13: ((Partial_Sums F) . l) . x <= ((Partial_Sums F) . k) . x by A4;
l >= n by A11, XREAL_1:19;
then ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . l) . x by A9, A12;
hence S₁[k] by A13, XXREAL_0:2; :: thesis: verum

end;

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

end;

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

end;

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