X, card X are_equipotent by CARD_1:def 5;
then consider f being Function such that
A1: ( f is one-to-one & dom f = X & rng f = card X ) by WELLORD2:def 4;
reconsider f = f as Function of X,(card X) by A1, FUNCT_2:4;
take f ; :: thesis: ( f is one-to-one & f is onto )
thus f is one-to-one by A1; :: thesis: f is onto
thus rng f = card X by A1; :: according to FUNCT_2:def 3 :: thesis: verum