let X, Y be set ; :: thesis:
thus ( card X c= card Y implies ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y ) ) :: thesis:

proof

assume A1: card X c= card Y ; :: thesis:
A2: ( X, card X are_equipotent & Y, card Y are_equipotent ) by Def5;
then consider f being Function such that
A3: ( f is one-to-one & dom f = X & rng f = card X ) by WELLORD2:def 4;
consider g being Function such that
A4: ( g is one-to-one & dom g = Y & rng g = card Y ) by A2, WELLORD2:def 4;
take h = (g " ) * f; :: thesis:
thus h is one-to-one by A3, A4; :: thesis:
( rng g = dom (g " ) & dom g = rng (g " ) ) by A4, FUNCT_1:55;
hence ( dom h = X & rng h c= Y ) by A1, A3, A4, RELAT_1:45, RELAT_1:46; :: thesis:

end;

given f being Function such that A5: ( f is one-to-one & dom f = X & rng f c= Y ) ; :: thesis:
Y, card Y are_equipotent by Def5;
then consider g being Function such that
A6: ( g is one-to-one & dom g = Y & rng g = card Y ) by WELLORD2:def 4;
A7: X, rng (g * f) are_equipotent

proof

take g * f ; :: according to WELLORD2:def 4 :: thesis:
thus g * f is one-to-one by A5, A6; :: thesis:
thus dom (g * f) = X by A5, A6, RELAT_1:46; :: thesis:
thus rng (g * f) = rng (g * f) ; :: thesis:

end;

A8: card (rng (g * f)) c= card Y by A6, Th23, RELAT_1:45;
( X, card X are_equipotent & rng (g * f), card (rng (g * f)) are_equipotent ) by Def5;
then ( card X,X are_equipotent & X, card (rng (g * f)) are_equipotent ) by A7, WELLORD2:22;
then card X, card (rng (g * f)) are_equipotent by WELLORD2:22;
hence card X c= card Y by A8, Th8; :: thesis: