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