theorem :: CHORD:14

for p being FinSequence
for n being non zero Nat st p is one-to-one & n <= len p holds
(p . n) .. p = n