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_{1}[ 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

S_{1}[l] ) holds

S_{1}[k]

S_{1}[k]
from NAT_1:sch 9(A8);

hence ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x by A4; :: thesis: verum

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

A5: for k being Nat holds ((Partial_Sums F) . k) . x <= ((Partial_Sums F) . (k + 1)) . x

proof

A8:
for k being Nat st k >= n & ( for l being Nat st l >= n & l < k holds
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;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

S

S

proof

for k being Nat st k >= n holds
let k be Nat; :: thesis: ( k >= n & ( for l being Nat st l >= n & l < k holds

S_{1}[l] ) implies S_{1}[k] )

assume A9: ( k >= n & ( for l being Nat st l >= n & l < k holds

S_{1}[l] ) )
; :: thesis: S_{1}[k]

_{1}[k]
by A9, XXREAL_0:1; :: thesis: verum

end;S

assume A9: ( k >= n & ( for l being Nat st l >= n & l < k holds

S

now :: thesis: ( k > n implies S_{1}[k] )

hence
Sassume
k > n
; :: thesis: S_{1}[k]

then k >= n + 1 by NAT_1:13;

then A10: ( k = n + 1 or k > n + 1 ) by XXREAL_0:1;

_{1}[k]
by A10, A5; :: thesis: verum

end;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_{1}[k] )

hence
Sassume A11:
k > n + 1
; :: thesis: S_{1}[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_{1}[k]
by A12, XXREAL_0:2; :: thesis: verum

end;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

S

hence ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x by A4; :: thesis: verum