theorem Th68: :: FINSEQ_5:68

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st len f <= n holds
Ins (f,n,p) = f ^ <*p*>