theorem Th11: :: FINSEQ_6:137

for p being FinSequence
for m, n being Nat holds rng ((m,n) -cut p) c= rng p