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 ; :: 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:
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 ;
then y in f .: X by ;
hence y in Y by A4; :: thesis: verum
end;
( f | X is one-to-one & dom (f | X) = X ) by ;
hence card X c= card Y by ; :: thesis: verum