theorem Th6: :: MEASURE9:8

for D being set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for m1, m2, k1, k2 being Nat st 1 <= m1 & 1 <= m2 & m1 + (Sum (Length (F | k1))) = m2 + (Sum (Length (F | k2))) & m1 + (Sum (Length (F | k1))) <= Sum (Length (F | (k1 + 1))) & m2 + (Sum (Length (F | k2))) <= Sum (Length (F | (k2 + 1))) holds
( m1 = m2 & k1 = k2 )