theorem :: FINSEQ_4:93

for m being Nat
for D being non empty set
for f being FinSequence of D st m in dom f holds
f /. m = (f | m) /. (len (f | m))