for i being Element of NAT
for a being set
for p, q being FinSequence st p +* (i,a) = q +* (i,a) holds
Del (p,i) = Del (q,i)