let X, Y be set ; :: thesis: ( card X c= card Y iff ex f being Function st X c= f .: Y )
thus ( card X c= card Y implies ex f being Function st X c= f .: Y ) :: thesis: ( ex f being Function st X c= f .: Y implies card X c= card Y )

proof

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

end;

given f being Function such that A2: X c= f .: Y ; :: thesis: card X c= card Y
deffunc H₁( set ) -> set = f . $1;
deffunc H₂( set ) -> set = $1;
defpred S₁[ set ] means $1 in dom f;
consider g being Function such that
A3: ( dom g = Y & ( for x being set st x in Y holds
( ( S₁[x] implies g . x = H₁(x) ) & ( not S₁[x] implies g . x = H₂(x) ) ) ) ) from PARTFUN1:sch 1();
X c= rng g

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in rng g )
assume x in X ; :: thesis: x in rng g
then consider y being set such that
A4: ( y in dom f & y in Y & x = f . y ) by A2, FUNCT_1:def 12;
( y in dom g & x = g . y ) by A3, A4;
hence x in rng g by FUNCT_1:def 5; :: thesis: verum

end;

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