theorem :: FINSEQ_5:73

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st n <= len f holds
(Ins (f,n,p)) . (n + 1) = p