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:33;
then dom p, rng p are_equipotent by RELAT_1:113;
then Seg (len p), rng p are_equipotent by FINSEQ_1:def 3;
then card (Seg (len p)) = card (rng p) by CARD_1:5;
hence card (rng p) = len p by FINSEQ_1:57; :: thesis: verum
end;
reconsider f = p as Function of (dom p),(rng p) by FUNCT_2:1;
reconsider B = dom p as finite set ;
assume card (rng p) = len p ; :: thesis: p is one-to-one
then card (rng p) = card (Seg (len p)) by FINSEQ_1:57;
then A1: card (rng p) = card B by FINSEQ_1:def 3;
f is onto by FUNCT_2:def 3;
hence p is one-to-one by Lm1, A1; :: thesis: verum