reconsider X = MonFuncs A,B as Subset of (Funcs the carrier of A,the carrier of B) by Th11;
X is functional ;
hence MonFuncs A,B is functional ; :: thesis: verum