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:
let n be Nat; :: thesis:
defpred S₁[ Nat] means $1 < (Partial_Sums (Length s)) . $1;
A1: for k being Nat holds len (s . k) >= 1

let k be Nat; :: thesis:
dom s = NAT by FUNCT_2:def 1;
then k in dom s by ORDINAL1:def 12;
hence len (s . k) >= 1 by FINSEQ_1:20; :: thesis:

end;

(Partial_Sums (Length s)) . 0 = (Length s) . 0 by SERIES_1:def 1
.= len (s . 0) by Def3 ;
then A3: S₁[ 0 ] ;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A5: S₁[k] ; :: thesis:
A6: (Partial_Sums (Length s)) . (k + 1) = ((Partial_Sums (Length s)) . k) + ((Length s) . (k + 1)) by SERIES_1:def 1;
(Length s) . (k + 1) = len (s . (k + 1)) by Def3;
hence S₁[k + 1] by A1, A6, A5, XREAL_1:8; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
hence ( len (s . n) >= 1 & n < (Partial_Sums (Length s)) . n ) by A1; :: thesis:
(Partial_Sums (Length s)) . (n + 1) = ((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 ;
hence (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . (n + 1) by XREAL_1:29; :: thesis: