let X, Y be non empty finite set ; :: thesis: ( card Y = card X implies ex f being Function of X,Y st f is bijective )
assume card Y = card X ; :: thesis: ex f being Function of X,Y st f is bijective
then X,Y are_equipotent by CARD_1:5;
then consider f being Function such that
F: ( f is one-to-one & dom f = X & rng f = Y ) by WELLORD2:def 4;
reconsider f = f as Function of X,Y by F, FUNCT_2:1;
take f ; :: thesis: f is bijective
f is onto by F, FUNCT_2:def 3;
hence f is bijective by F; :: thesis: verum