:: deftheorem defines <REAL,+> MONOID_0:def 26 :
<REAL,+> = multMagma(# REAL,addreal #);