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