A1: the carrier of (GFuncs X) = Funcs (X,X) by Def40;
id X in Funcs (X,X) by FUNCT_2:9;
hence ( GFuncs X is unital & not GFuncs X is empty ) by A1, Th71; :: thesis: verum