rng
f
=
X
by
Th7
;
then
A1
:
dom
(
f
"
)
=
X
by
FUNCT_1:33
;
dom
f
=
card
X
by
Th7
;
then
rng
(
f
"
)
=
card
X
by
FUNCT_1:33
;
hence
f
"
is
Enumeration
of
X
by
A1
,
Th6
;
:: thesis:
verum