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
A1: dom f = X and
A2: rng f c= {} by Def2;
rng f = {} by A2;
hence contradiction by A1, RELAT_1:65; :: thesis: verum