theorem Th7: :: NAT_5:7

for n being Nat
for f being FinSequence st f is one-to-one & n in dom f holds
not f . n in rng (Del (f,n))