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

X is functional ;

hence MonFuncs (A,B) is functional ; :: thesis: verum