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
for n being Nat holds
( len (s . n) >= 1 & n < (Partial_Sums (Length s)) . n & (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . (n + 1) )
let Y be non empty with_non-empty_element FinSequenceSet of D; :: thesis: for s being non-empty sequence of Y
for n being Nat holds
( len (s . n) >= 1 & n < (Partial_Sums (Length s)) . n & (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . (n + 1) )
let s be non-empty sequence of Y; :: thesis: for n being Nat holds
( len (s . n) >= 1 & n < (Partial_Sums (Length s)) . n & (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . (n + 1) )
let n be Nat; :: thesis: ( len (s . n) >= 1 & n < (Partial_Sums (Length s)) . n & (Partial_Sums (Length s)) . n < (Partial_Sums (Length s)) . (n + 1) )
defpred S₁[ Nat] means $1 < (Partial_Sums (Length s)) . $1;
A1: for k being Nat holds len (s . k) >= 1

proof

let k be Nat; :: thesis: len (s . k) >= 1
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: verum

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]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
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: verum

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 < (Partial_Sums (Length s)) . (n + 1)
(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: verum