for p being FinSequence holds
( p is one-to-one iff card (rng p) = len p )