let D be non empty set ; :: thesis: for Y being non empty with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y holds Partial_Sums (Length s) is increasing
let Y be non empty with_non-empty_element FinSequenceSet of D; :: thesis: for s being non-empty sequence of Y holds Partial_Sums (Length s) is increasing
let s be non-empty sequence of Y; :: thesis: Partial_Sums (Length s) is increasing

now :: thesis: for n, m being Nat st n in dom (Partial_Sums (Length s)) & m in dom (Partial_Sums (Length s)) & n < m holds
(Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . m

let n, m be Nat; :: thesis: ( n in dom (Partial_Sums (Length s)) & m in dom (Partial_Sums (Length s)) & n < m implies (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . m )
assume A1: ( n in dom (Partial_Sums (Length s)) & m in dom (Partial_Sums (Length s)) & n < m ) ; :: thesis: (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . m
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: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
(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: verum

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: verum

end;

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