let X be set ; :: thesis: Funcs X,{} = {}
dom (Funcs X,{} ) = dom {} by Def9;
hence Funcs X,{} = {} ; :: thesis: verum