theorem :: FINSEQ_5:75

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st 1 <= n & not f is empty holds
(Ins (f,n,p)) /. 1 = f /. 1