let A, B be finite set ; :: thesis: for f being Function of A,B st card A = card B & rng f = B holds
f is one-to-one
let f be Function of A,B; :: thesis: ( card A = card B & rng f = B implies f is one-to-one )
assume that
A1: card A = card B and
A2: rng f = B ; :: thesis: f is one-to-one
consider p being FinSequence such that
A3: rng p = A and
A4: p is one-to-one by Th73;
consider q being FinSequence such that
A5: rng q = B and
A6: q is one-to-one by Th73;
( dom p,p .: (dom p) are_equipotent & dom q,q .: (dom q) are_equipotent ) by A4, A6, CARD_1:60;
then ( dom p,A are_equipotent & dom q,B are_equipotent & A,B are_equipotent ) by A1, A3, A5, CARD_1:21, RELAT_1:146;
then ( dom p,B are_equipotent & B, dom q are_equipotent ) by WELLORD2:22;
then A7: ( dom p, dom q are_equipotent & dom q = Seg (len q) & Seg (len q) is finite ) by FINSEQ_1:def 3, WELLORD2:22;
reconsider X = dom p as finite set ;
card X = card (Seg (len q)) by A7, CARD_1:21
.= len q by FINSEQ_1:78 ;
then A8: len q = card (Seg (len p)) by FINSEQ_1:def 3
.= len p by FINSEQ_1:78 ;

now

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

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

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

end;

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

dom (q " ) = rng q by A6, FUNCT_1:55;
then rng f c= dom (q " ) by A5, RELAT_1:def 19;
then dom ((q " ) * f) = dom f by RELAT_1:46;
then rng p = dom ((q " ) * f) by A3, A9, FUNCT_2:def 1;
then A10: dom (((q " ) * f) * p) = dom p by RELAT_1:46
.= Seg (len p) by FINSEQ_1:def 3 ;
then reconsider g = ((q " ) * f) * p as FinSequence by FINSEQ_1:def 2;
A11: g = (q " ) * (f * p) by RELAT_1:55;
rng p = dom f by A3, A9, FUNCT_2:def 1;
then rng (f * p) = B by A2, RELAT_1:47
.= dom (q " ) by A5, A6, FUNCT_1:55 ;
then rng g = rng (q " ) by A11, RELAT_1:47
.= dom q by A6, FUNCT_1:55
.= Seg (len q) by FINSEQ_1:def 3 ;
then A12: g is one-to-one by A8, A10, Th75;
q * g = q * ((q " ) * (f * p)) by RELAT_1:55
.= (q * (q " )) * (f * p) by RELAT_1:55
.= (id (rng q)) * (f * p) by A6, FUNCT_1:61
.= ((id (rng q)) * f) * p by RELAT_1:55
.= f * p by A2, A5, RELAT_1:80 ;
then (q * g) * (p " ) = f * (p * (p " )) by RELAT_1:55
.= f * (id (rng p)) by A4, FUNCT_1:61
.= f * (id (dom f)) by A3, A9, FUNCT_2:def 1
.= f by RELAT_1:78 ;
hence f is one-to-one by A4, A6, A12; :: thesis: verum

end;

end;

end;

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