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