for p being FinSequence holds
( ( for n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n <> p . m ) iff p is one-to-one )