let X, Y be set ; :: thesis: ( card X c= card Y iff ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y ) )
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: ( ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y ) implies card X c= card Y )

proof

consider f being Function such that
A1: f is one-to-one and
A2: ( dom f = X & rng f = card X ) by Def2, WELLORD2:def 4;
assume A3: card X c= card Y ; :: thesis: ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y )
consider g being Function such that
A4: g is one-to-one and
A5: ( dom g = Y & rng g = card Y ) by Def2, WELLORD2:def 4;
take h = (g ") * f; :: thesis: ( h is one-to-one & dom h = X & rng h c= Y )
thus h is one-to-one by A1, A4; :: thesis: ( dom h = X & rng h c= Y )
( rng g = dom (g ") & dom g = rng (g ") ) by A4, FUNCT_1:33;
hence ( dom h = X & rng h c= Y ) by A3, A2, A5, RELAT_1:26, RELAT_1:27; :: thesis: verum

end;

given f being Function such that A6: f is one-to-one and
A7: ( dom f = X & rng f c= Y ) ; :: thesis: card X c= card Y
consider g being Function such that
A8: g is one-to-one and
A9: dom g = Y and
A10: rng g = card Y by Def2, WELLORD2:def 4;
A11: X, rng (g * f) are_equipotent

proof

take g * f ; :: according to WELLORD2:def 4 :: thesis: ( g * f is one-to-one & dom (g * f) = X & rng (g * f) = rng (g * f) )
thus g * f is one-to-one by A6, A8; :: thesis: ( dom (g * f) = X & rng (g * f) = rng (g * f) )
thus dom (g * f) = X by A7, A9, RELAT_1:27; :: thesis: rng (g * f) = rng (g * f)
thus rng (g * f) = rng (g * f) ; :: thesis: verum

end;

A12: rng (g * f), card (rng (g * f)) are_equipotent by Def2;
card (rng (g * f)) c= card Y by A10, Th6, RELAT_1:26;
hence card X c= card Y by A12, Def2, A11, WELLORD2:15; :: thesis: verum