:: deftheorem defines Ins FINSEQ_5:def 4 :
for D being non empty set
for f being FinSequence of D
for p being Element of D
for n being Nat holds Ins (f,n,p) = ((f | n) ^ <*p*>) ^ (f /^ n);