let X, Y be set ; :: thesis: ( card X c= card Y iff ex f being Function st X c= f .: Y )
deffunc H₂( set ) -> set = $1;
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 Th28;
take f ; :: thesis: X c= f .: Y
thus X c= f .: Y by A1, RELAT_1:113; :: thesis: verum

end;

given f being Function such that A2: X c= f .: Y ; :: thesis: card X c= card Y
defpred S₁[ set ] means $1 in dom f;
deffunc H₃( set ) -> set = f . $1;
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 and
A5: y in Y and
A6: x = f . y by A2, FUNCT_1:def 6;
x = g . y by A3, A4, A5, A6;
hence x in rng g by A3, A5, FUNCT_1:def 3; :: thesis: verum

end;

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