theorem Th7: :: MEASURE9:9

for D being non empty set
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) )