g * f is Function of X,Z ;
hence f * g is Element of Funcs X,Z by FUNCT_2:11; :: thesis: verum