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