let p be FinSequence; :: thesis: ( ( for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds
p . n <> p . m ) iff card (rng p) = len p )
( p is one-to-one iff card (rng p) = len p ) by FINSEQ_4:62;
hence ( ( for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds
p . n <> p . m ) iff card (rng p) = len p ) by Th9; :: thesis: verum