consider x being Element of Funcs X,Y;
assume not Funcs X,Y is empty ; :: thesis: contradiction
then consider f being Function such that
x = f and
A2: dom f = X and
A3: rng f c= {} by Def2;
rng f = {} by A3;
hence contradiction by A2, RELAT_1:65; :: thesis: verum