let f be Function; :: thesis: Funcs ({},f) = (dom f) --> {{}}

A1: now

let x be set ; :: thesis: ( x in dom f implies (Funcs ({},f)) . x = {{}} )
assume x in dom f ; :: thesis: (Funcs ({},f)) . x = {{}}
hence (Funcs ({},f)) . x = Funcs ({},(f . x)) by Def9
.= {{}} by FUNCT_5:64 ;
:: thesis: verum

end;

dom (Funcs ({},f)) = dom f by Def9;
hence Funcs ({},f) = (dom f) --> {{}} by A1, FUNCOP_1:17; :: thesis: verum