reconsider G0 = multMagma(# REAL,addreal #) as Group by Th3;
take G0 ; :: thesis: ( G0 is strict & G0 is commutative )
thus G0 is strict ; :: thesis: G0 is commutative
let a, g be Element of G0; :: according to GROUP_1:def 12 :: thesis: a * g = g * a
reconsider A = a, B = g as Real ;
thus a * g = B + A by BINOP_2:def 9
.= g * a by BINOP_2:def 9 ; :: thesis: verum