theorem :: GROUP_9:124

for D being non empty set
for f being FinSequence of D
for p being Element of D
for n being Nat st n in dom f holds
f = Del ((Ins (f,n,p)),(n + 1)) by Lm43;