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