X, card X are_equipotent
by CARD_1:def 2;

then consider f being Function such that

A1: f is one-to-one and

A2: dom f = X and

A3: rng f = card X by WELLORD2:def 4;

reconsider f = f as Function of X,(card X) by A2, A3, FUNCT_2:2;

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 A3; :: according to FUNCT_2:def 3 :: thesis: verum

then consider f being Function such that

A1: f is one-to-one and

A2: dom f = X and

A3: rng f = card X by WELLORD2:def 4;

reconsider f = f as Function of X,(card X) by A2, A3, FUNCT_2:2;

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 A3; :: according to FUNCT_2:def 3 :: thesis: verum