theorem Th11: :: FINSEQ_5:11

for i being Nat
for f being one-to-one FinSequence st i in dom f holds
(f . i) .. f = i