set f = the Function of X, the carrier of Y;
the Function of X, the carrier of Y in Funcs (X, the carrier of Y) by FUNCT_2:8;
hence not Y |^ X is empty by Th28; :: thesis: verum