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