let f be Function-yielding Function; ( {} in rng f implies <:f:> = {} )
A1: dom <:f:> =
meet (doms f)
by FUNCT_6:29
.=
meet (rng (doms f))
by FUNCT_6:def 4
;
assume
{} in rng f
; <:f:> = {}
then consider x being object such that
A2:
x in dom f
and
A3:
f . x = {}
by FUNCT_1:def 3;
A4:
dom (doms f) = dom f
by FUNCT_6:def 2;
then A5:
x in dom (doms f)
by A2;
then
(doms f) . x = {}
by A3, A4, FUNCT_6:def 2;
hence
<:f:> = {}
by A1, A5, FUNCT_1:3, SETFAM_1:4; verum