theorem Th4: :: COMPUT_1:4

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