let A, B be finite set ; :: thesis: for f being Function of A,B st card A = card B & f is onto holds
f is one-to-one
let f be Function of A,B; :: thesis: ( card A = card B & f is onto implies f is one-to-one )
assume that
A1: card A = card B and
A2: f is onto ; :: thesis: f is one-to-one
a2: rng f = B by A2, FUNCT_2:def 3;
A3: A,B are_equipotent by A1, CARD_1:5;
consider p being FinSequence such that
A4: rng p = A and
A5: p is one-to-one by Th58;
dom p,p .: (dom p) are_equipotent by A5, CARD_1:33;
then dom p,A are_equipotent by A4, RELAT_1:113;
then A6: dom p,B are_equipotent by A3, WELLORD2:15;
reconsider X = dom p as finite set ;
consider q being FinSequence such that
A7: rng q = B and
A8: q is one-to-one by Th58;
A9: dom q = Seg (len q) by FINSEQ_1:def 3;
dom q,q .: (dom q) are_equipotent by A8, CARD_1:33;
then dom q,B are_equipotent by A7, RELAT_1:113;
then dom p, dom q are_equipotent by A6, WELLORD2:15;
then card X = card (Seg (len q)) by A9, CARD_1:5
.= len q by FINSEQ_1:57 ;
then A10: len q = card (Seg (len p)) by FINSEQ_1:def 3
.= len p by FINSEQ_1:57 ;

now :: thesis: f is one-to-one

per cases ( B = {} or B <> {} ) ;

suppose B = {} ; :: thesis: f is one-to-one

hence f is one-to-one ; :: thesis: verum

end;

suppose A11: B <> {} ; :: thesis: f is one-to-one

then rng p = dom f by A4, FUNCT_2:def 1;
then A12: rng (f * p) = B by a2, RELAT_1:28
.= dom (q ") by A7, A8, FUNCT_1:33 ;
dom (q ") = rng q by A8, FUNCT_1:33;
then rng f c= dom (q ") by A7, RELAT_1:def 19;
then dom ((q ") * f) = dom f by RELAT_1:27;
then rng p = dom ((q ") * f) by A4, A11, FUNCT_2:def 1;
then A13: dom (((q ") * f) * p) = dom p by RELAT_1:27
.= Seg (len p) by FINSEQ_1:def 3 ;
then reconsider g = ((q ") * f) * p as FinSequence by FINSEQ_1:def 2;
g = (q ") * (f * p) by RELAT_1:36;
then rng g = rng (q ") by A12, RELAT_1:28
.= dom q by A8, FUNCT_1:33
.= Seg (len q) by FINSEQ_1:def 3 ;
then A14: g is one-to-one by A10, A13, Th60;
q * g = q * ((q ") * (f * p)) by RELAT_1:36
.= (q * (q ")) * (f * p) by RELAT_1:36
.= (id (rng q)) * (f * p) by A8, FUNCT_1:39
.= ((id (rng q)) * f) * p by RELAT_1:36
.= f * p by a2, A7, RELAT_1:54 ;
then (q * g) * (p ") = f * (p * (p ")) by RELAT_1:36
.= f * (id (rng p)) by A5, FUNCT_1:39
.= f * (id (dom f)) by A4, A11, FUNCT_2:def 1
.= f by RELAT_1:52 ;
hence f is one-to-one by A5, A8, A14; :: thesis: verum

end;

end;

end;

hence f is one-to-one ; :: thesis: verum