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