let A, B be finite set ; 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; ( 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
; rng f = B
A3:
A,B are_equipotent
by A1, CARD_1:21;
consider p being FinSequence such that
A4:
rng p = A
and
A5:
p is one-to-one
by Th73;
dom p,p .: (dom p) are_equipotent
by A5, CARD_1:60;
then
dom p,A are_equipotent
by A4, RELAT_1:146;
then A6:
dom p,B are_equipotent
by A3, WELLORD2:22;
consider q being FinSequence such that
A7:
rng q = B
and
A8:
q is one-to-one
by Th73;
A9:
dom q = Seg (len q)
by FINSEQ_1:def 3;
dom q,q .: (dom q) are_equipotent
by A8, CARD_1:60;
then
dom q,B are_equipotent
by A7, RELAT_1:146;
then
dom p, dom q are_equipotent
by A6, WELLORD2:22;
then card (dom p) =
card (Seg (len q))
by A9, CARD_1:21
.=
len q
by FINSEQ_1:78
;
then A10: len q =
card (Seg (len p))
by FINSEQ_1:def 3
.=
len p
by FINSEQ_1:78
;
per cases
( B = {} or B <> {} )
;
suppose A11:
B <> {}
;
rng f = B
dom (q " ) = rng q
by A8, FUNCT_1:55;
then
rng f c= dom (q " )
by A7, RELAT_1:def 19;
then
dom ((q " ) * f) = dom f
by RELAT_1:46;
then
rng p = dom ((q " ) * f)
by A4, 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 A8, FUNCT_1:55;
then
rng g c= dom g
by A10, A12, FINSEQ_1:def 3;
then
rng g = dom g
by A2, A5, A8, Th74;
then
rng g = dom q
by A10, A12, FINSEQ_1:def 3;
then A13:
rng (q * g) = B
by A7, RELAT_1:47;
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:55
.=
(q * (q " )) * (f * p)
by RELAT_1:55
.=
(id (rng q)) * (f * p)
by A8, FUNCT_1:61
.=
((id (rng q)) * f) * p
by RELAT_1:55
.=
f * p
by A14, RELAT_1:79
;
hence
rng f = B
by A13, A15, RELAT_1:47;
verum end;