theorem Th8: :: NAT_5:8

for n being Nat
for f being FinSequence
for x being set st x in rng f & not x in rng (Del (f,n)) holds
x = f . n