consider f being Function of X,the carrier of Y;
f in Funcs X,the carrier of Y by FUNCT_2:11;
hence not Y |^ X is empty by Th28; :: thesis: verum