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

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

suppose B = {} ; :: thesis: rng f = B

hence rng f = B ; :: thesis: verum

end;

suppose A11: B <> {} ; :: thesis: rng f = B

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, A11, FUNCT_2:def 1;
then A12: 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;
g = (q " ) * (f * p) by RELAT_1:55;
then rng g c= rng (q " ) by RELAT_1:45;
then rng g c= dom q by A6, FUNCT_1:55;
then A13: rng g c= dom g by A8, A12, FINSEQ_1:def 3;
(q " ) * f is one-to-one by A2, A6;
then A14: rng g = dom g by A13, Th74, A4;
A15: rng f c= rng q by A5, RELAT_1:def 19;
A16: 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 A15, RELAT_1:79 ;
rng g = dom q by A8, A12, A14, FINSEQ_1:def 3;
then A17: rng (q * g) = B by A5, RELAT_1:47;
rng p = dom f by A3, A11, FUNCT_2:def 1;
hence rng f = B by A16, A17, RELAT_1:47; :: thesis: verum

end;

end;