theorem Th13: :: TOPREAL8:13

for k being Nat
for D being set
for f being FinSequence of D st 1 <= k holds
((k + 1),(len f)) -cut f = f /^ k