theorem Th73: :: MEASUR11:2

for F being FinSequence
for m, n being Nat st m <= n holds
len (F | m) <= len (F | n)