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 object such that
A3: x1 in dom F and
A4: x2 in dom F and
A5: F . x1 = F . x2 and
A6: x1 <> x2 ;
reconsider Xx = X \ {x1} as finite set ;
Y c= F .: Xx

proof

let Fy be object ; :: 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 object such that
A7: y in dom F and
A8: F . y = Fy by FUNCT_1:def 3;

now :: thesis: Fy in F .: Xx

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

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

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

end;

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

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

end;

end;

end;

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

end;

then A10: Segm (card Y) c= Segm (card Xx) by CARD_1:66;
{x1} meets X by A3, ZFMISC_1:48;
then A11: Xx <> X by XBOOLE_1:83;
Xx c< X by A11;
hence contradiction by A1, A10, NAT_1:39, CARD_2:48; :: 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 A12: card (dom F) = card (F .: (dom F)) by CARD_1:5, CARD_1:33;
assume not F is onto ; :: thesis: contradiction
then not rng F = Y by FUNCT_2:def 3;
then not Y c= rng F ;
then consider y being object such that
A13: y in Y and
A14: not y in rng F ;
A15: card (rng F) <= card (Y \ {y}) by A14, NAT_1:43, ZFMISC_1:34;
A16: F .: (dom F) = rng F by RELAT_1:113;
{y} meets Y by A13, ZFMISC_1:48;
then A17: Y \ {y} <> Y by XBOOLE_1:83;
Y \ {y} c< Y by A17;
then card (Y \ {y}) < card Y by CARD_2:48;
hence contradiction by A1, A13, A15, A12, A16, FUNCT_2:def 1; :: thesis: verum

end;