theorem Th3: :: MEASURE9:5

for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for n being Nat st 1 <= n & n <= Sum (Length F) holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) )