for p being FinSequence holds
( ( for n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n <> p . m ) iff card (rng p) = len p ) by Th4, FINSEQ_4:62;