let f be Function; :: thesis: ( {} in rng f implies <:f:> = {} )
assume A1: {} in rng f ; :: thesis: <:f:> = {}
A2: dom <:f:> = meet (doms f) by FUNCT_6:49
.= meet (rng (doms f)) by FUNCT_6:def 4 ;
consider x being set such that
A3: ( x in dom f & f . x = {} ) by A1, FUNCT_1:def 5;
A4: dom (doms f) = f " (SubFuncs (rng f)) by FUNCT_6:def 2;
then A5: x in dom (doms f) by A3, FUNCT_6:28;
then (doms f) . x = {} by A3, A4, FUNCT_5:10, FUNCT_6:def 2;
then meet (rng (doms f)) = {} by A5, FUNCT_1:12, SETFAM_1:5;
hence <:f:> = {} by A2; :: thesis: verum