set
a
= the
Element
of
A
;
dom
f
=
A
by
Th19
;
then
f
.
the
Element
of
A
in
rng
f
by
FUNCT_1:def 3
;
hence
not
rng
f
is
empty
;
:: thesis:
verum