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

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