:: deftheorem defines MFuncs MONOID_0:def 41 :
for X being set
for b₂ being strict well-unital MonoidalExtension of GFuncs X holds
( b₂ = MFuncs X iff verum );