theorem Th3: :: COMPUT_1:3

for x being set
for p being FinSequence
for i being Nat holds Del ((p +* (i,x)),i) = Del (p,i)