let f be Function; :: thesis: ( not {} in rng f implies Funcs (f,{}) = (dom f) --> {} )
assume A1: not {} in rng f ; :: thesis: Funcs (f,{}) = (dom f) --> {}

A2: now

let x be set ; :: thesis: ( x in dom f implies ((dom f) --> {}) . x = Funcs ((f . x),{}) )
assume A3: x in dom f ; :: thesis: ((dom f) --> {}) . x = Funcs ((f . x),{})
then A4: f . x <> {} by A1, FUNCT_1:def 3;
thus ((dom f) --> {}) . x = {} by A3, FUNCOP_1:7
.= Funcs ((f . x),{}) by A4 ; :: thesis: verum

end;

dom ((dom f) --> {}) = dom f by FUNCOP_1:13;
hence Funcs (f,{}) = (dom f) --> {} by A2, Def8; :: thesis: verum