theorem Th5: :: MEASURE9:7

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