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