set R = multMagma(# REAL ,multreal #);
( multMagma(# REAL ,multreal #) is unital & multMagma(# REAL ,multreal #) is commutative & multMagma(# REAL ,multreal #) is associative )

proof

thus ( H₂( multMagma(# REAL ,multreal #)) is having_a_unity & H₂( multMagma(# REAL ,multreal #)) is commutative & H₂( multMagma(# REAL ,multreal #)) is associative ) ; :: according to MONOID_0:def 10,MONOID_0:def 11,MONOID_0:def 12 :: thesis: verum

end;

hence multMagma(# REAL ,multreal #) is non empty strict unital associative commutative multMagma ; :: thesis: verum