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 5;
then consider P being Function such that
A1: ( P is one-to-one & dom P = card X & rng P = X ) by WELLORD2:def 4;
P is Function of (card X),X by A1, FUNCT_2:3;
hence ex P being Function of (card X),X st P is one-to-one by A1; :: thesis: verum