theorem Th61: :: NUMBER19:61

for z being FinSequence
for i being Nat st z is_one-to-one_at i holds
rng (Del (z,i)) = (rng z) \ {(z . i)}