set f = the Function of X,L;
the Function of X,L in Funcs (X, the carrier of L) by FUNCT_2:8;
hence not Maps (X,L) is empty by defmap; :: thesis: verum