let D be non empty set ; :: thesis:
let Y be non empty with_non-empty_element FinSequenceSet of D; :: thesis:
let s be non-empty sequence of Y; :: thesis:

now :: thesis:

let n, m be Nat; :: thesis:
assume A1: ( n in dom (Partial_Sums (Length s)) & m in dom (Partial_Sums (Length s)) & n < m ) ; :: thesis:
defpred S₁[ Nat] means (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . ((n + 1) + $1);
(Partial_Sums (Length s)) . ((n + 1) + 0) = ((Partial_Sums (Length s)) . n) + ((Length s) . (n + 1)) by SERIES_1:def 1
.= ((Partial_Sums (Length s)) . n) + (len (s . (n + 1))) by Def3 ;
then A3: S₁[ 0 ] by XREAL_1:29;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A5: S₁[k] ; :: thesis:
(Partial_Sums (Length s)) . ((n + 1) + (k + 1)) = ((Partial_Sums (Length s)) . ((n + 1) + k)) + ((Length s) . (((n + 1) + k) + 1)) by SERIES_1:def 1
.= ((Partial_Sums (Length s)) . ((n + 1) + k)) + (len (s . (((n + 1) + k) + 1))) by Def3 ;
then (Partial_Sums (Length s)) . ((n + 1) + (k + 1)) > (Partial_Sums (Length s)) . ((n + 1) + k) by XREAL_1:29;
hence S₁[k + 1] by A5, XXREAL_0:2; :: thesis:

end;

A7: for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
n + 1 <= m by A1, NAT_1:13;
then reconsider k = m - (n + 1) as Nat by NAT_1:21;
m = (n + 1) + k ;
hence (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . m by A7; :: thesis:

end;

hence Partial_Sums (Length s) is increasing by SEQM_3:def 1; :: thesis: