reconsider f = f, g = g as Function of M,M ;
g * f in Funcs ( the carrier of M, the carrier of M) by FUNCT_2:9;
hence f * g is Element of Funcs ( the carrier of M, the carrier of M) ; :: thesis: verum