:: deftheorem Def1 defines constituted-Functions MONOID_0:def 1 :
for IT being 1-sorted holds
( IT is constituted-Functions iff for a being Element of IT holds a is Function );