for f being CR_Sequence
for m being Nat st 0 < m & m <= len f holds
f | m is CR_Sequence