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