let A, B be finite set ; :: thesis: for f being Function of A,B st card A = card B & f is one-to-one holds
f is onto
let f be Function of A,B; :: thesis: ( card A = card B & f is one-to-one implies f is onto )
assume that
A1: card A = card B and
A2: f is one-to-one ; :: thesis: f is onto
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;
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 (dom p) = 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 ;

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

suppose B = {} ; :: thesis: f is onto

then rng f = B ;
hence f is onto by FUNCT_2:def 3; :: thesis: verum

end;

suppose A11: B <> {} ; :: thesis: f is onto

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 A12: 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 c= rng (q ") by RELAT_1:26;
then rng g c= dom q by A8, FUNCT_1:33;
then rng g c= dom g by A10, A12, FINSEQ_1:def 3;
then rng g = dom g by A2, A5, A8, Th59;
then rng g = dom q by A10, A12, FINSEQ_1:def 3;
then A13: rng (q * g) = B by A7, RELAT_1:28;
A14: rng f c= rng q by A7, RELAT_1:def 19;
A15: rng p = dom f by A4, A11, FUNCT_2:def 1;
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 A14, RELAT_1:53 ;
then rng f = B by A13, A15, RELAT_1:28;
hence f is onto by FUNCT_2:def 3; :: thesis: verum

end;

end;