theorem Th58: :: FINSEQ_6:58

for i, k being Nat
for D being non empty set
for f being FinSequence of D st k < i & i in dom f holds
f /. i in rng (f /^ k)