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 :: thesis: for x being object st x in dom f holds
((dom f) --> {}) . x = Funcs ((f . x),{})

let x be object ; :: thesis: ( x in dom f implies ((dom f) --> {}) . x = Funcs ((f . x),{}) )
assume 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 = {}
.= Funcs ((f . x),{}) by A4 ; :: thesis: verum

end;

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