let A, B be finite set ; for f being Function of A,B st card A = card B & f is onto holds
f is one-to-one
let f be Function of A,B; ( card A = card B & f is onto implies f is one-to-one )
assume that
A1:
card A = card B
and
A2:
f is onto
; f is one-to-one
a2:
rng f = B
by A2, FUNCT_2:def 3;
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;
reconsider X = dom p as finite set ;
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 X =
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
;
now f is one-to-one per cases
( B = {} or B <> {} )
;
suppose A11:
B <> {}
;
f is one-to-one then
rng p = dom f
by A4, FUNCT_2:def 1;
then A12:
rng (f * p) =
B
by a2, RELAT_1:28
.=
dom (q ")
by A7, A8, FUNCT_1:33
;
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 A13:
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 =
rng (q ")
by A12, RELAT_1:28
.=
dom q
by A8, FUNCT_1:33
.=
Seg (len q)
by FINSEQ_1:def 3
;
then A14:
g is
one-to-one
by A10, A13, Th60;
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 a2, A7, RELAT_1:54
;
then (q * g) * (p ") =
f * (p * (p "))
by RELAT_1:36
.=
f * (id (rng p))
by A5, FUNCT_1:39
.=
f * (id (dom f))
by A4, A11, FUNCT_2:def 1
.=
f
by RELAT_1:52
;
hence
f is
one-to-one
by A5, A8, A14;
verum end;
hence
f is one-to-one
; verum