let X be finite set ; :: thesis: ex P being Function of (card X),X st P is one-to-one
card X,X are_equipotent by CARD_1:def 2;
then consider P being Function such that
A1: P is one-to-one and
A2: ( dom P = card X & rng P = X ) by WELLORD2:def 4;
P is Function of (card X),X by A2, FUNCT_2:1;
hence ex P being Function of (card X),X st P is one-to-one by A1; :: thesis: verum