let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL
for x being Element of X st F is with_the_same_dom & x in dom (F . 0) & ( for m being Nat holds F . m is nonnegative ) holds
( (Partial_Sums F) # x is non-decreasing & (Partial_Sums F) # x is convergent )
let F be Functional_Sequence of X,ExtREAL; :: thesis: for x being Element of X st F is with_the_same_dom & x in dom (F . 0) & ( for m being Nat holds F . m is nonnegative ) holds
( (Partial_Sums F) # x is non-decreasing & (Partial_Sums F) # x is convergent )
let x be Element of X; :: thesis: ( F is with_the_same_dom & x in dom (F . 0) & ( for m being Nat holds F . m is nonnegative ) implies ( (Partial_Sums F) # x is non-decreasing & (Partial_Sums F) # x is convergent ) )
assume A1: F is with_the_same_dom ; :: thesis: ( not x in dom (F . 0) or ex m being Nat st not F . m is nonnegative or ( (Partial_Sums F) # x is non-decreasing & (Partial_Sums F) # x is convergent ) )
assume A2: x in dom (F . 0) ; :: thesis: ( ex m being Nat st not F . m is nonnegative or ( (Partial_Sums F) # x is non-decreasing & (Partial_Sums F) # x is convergent ) )
assume A3: for m being Nat holds F . m is nonnegative ; :: thesis: ( (Partial_Sums F) # x is non-decreasing & (Partial_Sums F) # x is convergent )
for n, m being Nat st m <= n holds
((Partial_Sums F) # x) . m <= ((Partial_Sums F) # x) . n
proof
let n, m be Nat; :: thesis: ( m <= n implies ((Partial_Sums F) # x) . m <= ((Partial_Sums F) # x) . n )
assume m <= n ; :: thesis: ((Partial_Sums F) # x) . m <= ((Partial_Sums F) # x) . n
then ((Partial_Sums F) . m) . x <= ((Partial_Sums F) . n) . x by A1, A2, A3, Th37;
then ((Partial_Sums F) # x) . m <= ((Partial_Sums F) . n) . x by MESFUNC5:def 13;
hence ((Partial_Sums F) # x) . m <= ((Partial_Sums F) # x) . n by MESFUNC5:def 13; :: thesis: verum
end;
hence (Partial_Sums F) # x is non-decreasing by RINFSUP2:7; :: thesis: (Partial_Sums F) # x is convergent
hence (Partial_Sums F) # x is convergent by RINFSUP2:37; :: thesis: verum