theorem :: MONOID_0:76

for X being set holds
( the carrier of (MFuncs X) = Funcs (X,X) & the multF of (MFuncs X) = (X -composition) || (Funcs (X,X)) & 1. (MFuncs X) = id X )