let A, B be finite set ; 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; ( 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
; 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 A11:
B <> {}
;
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;
verum end;