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 5;
thus ((dom f) --> {} ) . x = {} by A3, FUNCOP_1:13
.= Funcs (f . x),{} by A4 ; :: thesis: verum

end;

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