theorem Th63: :: FINSEQ_6:63

for k being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds
f /. k in rng (f :- p)