theorem :: FINSEQ_5:67

for D being non empty set
for p being Element of D
for f being FinSequence of D holds Ins (f,0,p) = <*p*> ^ f by FINSEQ_1:34;