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 ;
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 ;
hence Fy in F .: Xx by ; :: thesis: verum
end;
suppose y <> x1 ; :: thesis: Fy in F .: Xx
then y in Xx by ;
hence Fy in F .: Xx by ; :: 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;
card Xx < card X by ;
then Segm (card Xx) c< Segm (card X) by NAT_1:39;
then Segm (card X) c< Segm (card Y) by ;
hence contradiction by A1; :: 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:33;
then A11: card (dom F) = card (F .: (dom F)) by CARD_1:5;
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
A12: y in Y and
A13: not y in rng F ;
A14: card (rng F) <= card (Y \ {y}) by ;
A15: F .: (dom F) = rng F by RELAT_1:113;
card (Y \ {y}) < card Y by ;
hence contradiction by A1, A12, A14, A11, A15, FUNCT_2:def 1; :: thesis: verum
end;