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

A1: now :: thesis: for x being object st x in dom f holds
(Funcs ({},f)) . x = {{}}

let x be object ; :: 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 Def8
.= {{}} by FUNCT_5:57 ;
:: thesis: verum

end;

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