reconsider f = f, g = g as Function of X,X by FUNCT_2:121;
g * f in Funcs X,X by FUNCT_2:12;
hence f * g is Element of Funcs X,X ; :: thesis: verum