let X, Y be finite set ; :: thesis: for F being Function of X,Y st card X = card Y holds
( F is onto iff F is one-to-one )
let F be Function of X,Y; :: thesis: ( card X = card Y implies ( F is onto iff F is one-to-one ) )
assume A1: card X = card Y ; :: thesis: ( F is onto iff F is one-to-one )
thus ( F is onto implies F is one-to-one ) :: thesis: ( F is one-to-one implies F is onto )

proof

assume A2: F is onto ; :: thesis: F is one-to-one
assume not F is one-to-one ; :: thesis: contradiction
then consider x1, x2 being set such that
A3: x1 in dom F and
A4: x2 in dom F and
A5: F . x1 = F . x2 and
A6: x1 <> x2 by FUNCT_1:def 8;
reconsider Xx = X \ {x1} as finite set ;
Y c= F .: Xx

proof

let Fy be set ; :: according to TARSKI:def 3 :: thesis: ( not Fy in Y or Fy in F .: Xx )
assume Fy in Y ; :: thesis: Fy in F .: Xx
then Fy in rng F by A2, FUNCT_2:def 3;
then consider y being set such that
A7: y in dom F and
A8: F . y = Fy by FUNCT_1:def 5;

now

per cases ( y = x1 or y <> x1 ) ;

suppose A9: y = x1 ; :: thesis: Fy in F .: Xx

x2 in Xx by A4, A6, ZFMISC_1:64;
hence Fy in F .: Xx by A4, A5, A8, A9, FUNCT_1:def 12; :: thesis: verum

end;

suppose y <> x1 ; :: thesis: Fy in F .: Xx

then y in Xx by A7, ZFMISC_1:64;
hence Fy in F .: Xx by A7, A8, FUNCT_1:def 12; :: thesis: verum

end;

end;

end;

hence Fy in F .: Xx ; :: thesis: verum

end;

then A10: card Y c= card Xx by CARD_2:2;
{x1} meets X by A3, ZFMISC_1:54;
then A11: Xx <> X by XBOOLE_1:83;
Xx c< X by XBOOLE_0:def 8, A11;
then card Xx < card X by CARD_2:67;
hence contradiction by A1, A10, NAT_1:40; :: thesis: verum

end;

thus ( F is one-to-one implies F is onto ) :: thesis: verum

proof

assume F is one-to-one ; :: thesis: F is onto
then dom F,F .: (dom F) are_equipotent by CARD_1:60;
then A12: card (dom F) = card (F .: (dom F)) by CARD_1:21;
assume not F is onto ; :: thesis: contradiction
then not rng F = Y by FUNCT_2:def 3;
then not Y c= rng F by XBOOLE_0:def 10;
then consider y being set such that
A13: y in Y and
A14: not y in rng F by TARSKI:def 3;
A15: card (rng F) <= card (Y \ {y}) by A14, NAT_1:44, ZFMISC_1:40;
A16: F .: (dom F) = rng F by RELAT_1:146;
{y} meets Y by ZFMISC_1:54, A13;
then A17: Y \ {y} <> Y by XBOOLE_1:83;
Y \ {y} c< Y by XBOOLE_0:def 8, A17;
then card (Y \ {y}) < card Y by CARD_2:67;
hence contradiction by A1, A13, A15, A12, A16, FUNCT_2:def 1; :: thesis: verum

end;