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