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

proof

assume card X c= card Y ; :: thesis: ex f being Function st
( f is one-to-one & X c= dom f & f .: X c= Y )
then consider f being Function such that
A1: ( f is one-to-one & dom f = X & rng f c= Y ) by CARD_1:10;
take f ; :: thesis: ( f is one-to-one & X c= dom f & f .: X c= Y )
thus ( f is one-to-one & X c= dom f & f .: X c= Y ) by A1, RELAT_1:113; :: thesis: verum

end;

given f being Function such that A2: f is one-to-one and
A3: X c= dom f and
A4: f .: X c= Y ; :: thesis: card X c= card Y
A5: rng (f | X) c= Y

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f | X) or y in Y )
assume y in rng (f | X) ; :: thesis: y in Y
then consider x being object such that
A6: ( x in dom (f | X) & y = (f | X) . x ) by FUNCT_1:def 3;
( x in X & y = f . x ) by A3, A6, FUNCT_1:47, RELAT_1:62;
then y in f .: X by A3, FUNCT_1:def 6;
hence y in Y by A4; :: thesis: verum

end;

( f | X is one-to-one & dom (f | X) = X ) by A2, A3, FUNCT_1:52, RELAT_1:62;
hence card X c= card Y by A5, CARD_1:10; :: thesis: verum