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

proof

assume card X c= card Y ; :: thesis: ex f being Function st
( dom f = Y & X c= rng f )
then consider f being Function such that
A1: ( f is one-to-one & dom f = X & rng f c= Y ) by Th26;
defpred S₁[ set , set ] means ( ( $1 in rng f & $2 = (f " ) . $1 ) or ( not $1 in rng f & $2 = 0 ) );
A2: for x being set st x in Y holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in Y implies ex y being set st S₁[x,y] )
assume x in Y ; :: thesis: ex y being set st S₁[x,y]
( not x in rng f implies ex y being set st S₁[x,y] ) ;
hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

A3: for x, y, z being set st x in Y & S₁[x,y] & S₁[x,z] holds
y = z ;
consider g being Function such that
A4: ( dom g = Y & ( for y being set st y in Y holds
S₁[y,g . y] ) ) from FUNCT_1:sch 2(A3, A2);
take g ; :: thesis: ( dom g = Y & X c= rng g )
thus dom g = Y by A4; :: thesis: X c= rng g
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 A5: ( (f " ) . (f . x) = x & f . x in rng f ) by A1, FUNCT_1:56, FUNCT_1:def 5;
then x = g . (f . x) by A1, A4;
hence x in rng g by A1, A4, A5, FUNCT_1:def 5; :: thesis: verum

end;

given f being Function such that A6: ( dom f = Y & X c= rng f ) ; :: thesis: card X c= card Y
deffunc H₁( set ) -> set = f " {$1};
consider g being Function such that
A7: ( dom g = X & ( for x being set st x in X holds
g . x = H₁(x) ) ) from FUNCT_1:sch 3();
( X <> {} implies card X c= card Y )

proof

assume X <> {} ; :: thesis: card X c= card Y
then reconsider M = rng g as non empty set by A7, RELAT_1:65;
for Z being set st Z in M holds
Z <> {}

proof

let Z be set ; :: thesis: ( Z in M implies Z <> {} )
assume Z in M ; :: thesis: Z <> {}
then consider x being set such that
A8: ( x in dom g & Z = g . x ) by FUNCT_1:def 5;
A9: ( Z = f " {x} & x in rng f ) by A6, A7, A8;
consider y being set such that
A10: ( y in dom f & x = f . y ) by A6, A7, A8, FUNCT_1:def 5;
x in {x} by TARSKI:def 1;
hence Z <> {} by A9, A10, FUNCT_1:def 13; :: thesis: verum

end;

then consider F being Function such that
A11: ( dom F = M & ( for Z being set st Z in M holds
F . Z in Z ) ) by WELLORD2:28;
A12: dom (F * g) = X by A7, A11, RELAT_1:46;
A13: F * g is one-to-one

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom (F * g) or not b₁ in dom (F * g) or not (F * g) . x = (F * g) . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom (F * g) or not y in dom (F * g) or not (F * g) . x = (F * g) . y or x = y )
assume A14: ( x in dom (F * g) & y in dom (F * g) & (F * g) . x = (F * g) . y ) ; :: thesis: x = y
then A15: ( g . x = f " {x} & g . y = f " {y} & (F * g) . x = F . (g . x) & (F * g) . y = F . (g . y) ) by A7, A12, FUNCT_1:23;
then ( F . (f " {x}) = F . (f " {y}) & f " {x} in M & f " {y} in M ) by A7, A12, A14, FUNCT_1:def 5;
then ( F . (f " {x}) in f " {x} & F . (f " {y}) in f " {y} ) by A11;
then ( f . (F . (f " {x})) in {x} & f . (F . (f " {y})) in {y} ) by FUNCT_1:def 13;
then ( f . (F . (f " {x})) = x & f . (F . (f " {y})) = y ) by TARSKI:def 1;
hence x = y by A14, A15; :: thesis: verum

end;

rng (F * g) c= Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (F * g) or x in Y )
assume x in rng (F * g) ; :: thesis: x in Y
then consider y being set such that
A16: ( y in dom (F * g) & x = (F * g) . y ) by FUNCT_1:def 5;
A17: ( g . y = f " {y} & x = F . (g . y) ) by A7, A12, A16, FUNCT_1:23;
then f " {y} in M by A7, A12, A16, FUNCT_1:def 5;
then x in f " {y} by A11, A17;
hence x in Y by A6, FUNCT_1:def 13; :: thesis: verum

end;

hence card X c= card Y by A12, A13, Th26; :: thesis: verum

end;

hence card X c= card Y ; :: thesis: verum