theorem Th72: :: FINSEQ_5:72

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D
for i being Nat st i in dom (f | n) holds
(Ins (f,n,p)) . i = f . i