theorem :: GROUP_1:46

multMagma(# REAL,addreal #) is commutative Group