reconsider G = multMagma(# REAL,addreal #) as Group by Th3;
G is commutative

proof

let h, g be Element of G; :: according to GROUP_1:def 12 :: thesis: h * g = g * h
reconsider A = h, B = g as Real ;
thus h * g = B + A by BINOP_2:def 9
.= g * h by BINOP_2:def 9 ; :: thesis: verum

end;

hence multMagma(# REAL,addreal #) is commutative Group ; :: thesis: verum