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