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:26;
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:146; :: thesis: verum

end;

given f being Function such that A2: ( f is one-to-one & X c= dom f & f .: X c= Y ) ; :: thesis: card X c= card Y
A3: f | X is one-to-one by A2, FUNCT_1:84;
A4: dom (f | X) = X by A2, RELAT_1:91;
rng (f | X) c= Y

proof

let y be set ; :: 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 set such that
A5: ( x in dom (f | X) & y = (f | X) . x ) by FUNCT_1:def 5;
A6: x in X by A2, A5, RELAT_1:91;
then ( x in dom f & y = f . x ) by A2, A5, FUNCT_1:70;
then y in f .: X by A6, FUNCT_1:def 12;
hence y in Y by A2; :: thesis: verum

end;

hence card X c= card Y by A3, A4, CARD_1:26; :: thesis: verum