theorem Th6: :: NAT_5:6

for n being Nat
for f being FinSequence st f is one-to-one holds
Del (f,n) is one-to-one