theorem Th48: :: FINSEQ_6:48

for k being Nat
for D being non empty set
for f being FinSequence of D st k in dom f & ( for i being Nat st 1 <= i & i < k holds
f /. i <> f /. k ) holds
(f /. k) .. f = k