:: deftheorem defines <REAL,*> MONOID_0:def 30 :
<REAL,*> = multMagma(# REAL,multreal #);