let p be FinSequence; :: thesis: ( p is one-to-one iff card (rng p) = len p )
thus ( p is one-to-one implies card (rng p) = len p ) :: thesis: ( card (rng p) = len p implies p is one-to-one )

proof

assume p is one-to-one ; :: thesis: card (rng p) = len p
then dom p,p .: (dom p) are_equipotent by CARD_1:60;
then dom p, rng p are_equipotent by RELAT_1:146;
then ( Seg (len p), rng p are_equipotent & Seg (len p) is finite ) by FINSEQ_1:def 3;
then card (Seg (len p)) = card (rng p) by CARD_1:21;
hence card (rng p) = len p by FINSEQ_1:78; :: thesis: verum

end;

assume A1: card (rng p) = len p ; :: thesis: p is one-to-one
reconsider f = p as Function of (dom p),(rng p) by FUNCT_2:3;
A2: ( card (rng p) = card (Seg (len p)) & Seg (len p) is finite ) by A1, FINSEQ_1:78;
reconsider B = dom p as finite set ;
( card (rng p) = card B & dom f is finite ) by A2, FINSEQ_1:def 3;
hence p is one-to-one by Lm1; :: thesis: verum