thus addreal is commutative :: thesis: addreal is associative

proof

let r1 be Element of REAL ; :: according to BINOP_1:def 13 :: thesis: for b₁ being Element of REAL holds addreal . r1,b₁ = addreal . b₁,r1
let r2 be Element of REAL ; :: thesis: addreal . r1,r2 = addreal . r2,r1
thus addreal . r1,r2 = r1 + r2 by Def9
.= addreal . r2,r1 by Def9 ; :: thesis: verum

end;

let r1 be Element of REAL ; :: according to BINOP_1:def 14 :: thesis: for b₁, b₂ being Element of REAL holds addreal . r1,(addreal . b₁,b₂) = addreal . (addreal . r1,b₁),b₂
let r2, r3 be Element of REAL ; :: thesis: addreal . r1,(addreal . r2,r3) = addreal . (addreal . r1,r2),r3
thus addreal . r1,(addreal . r2,r3) = r1 + (addreal . r2,r3) by Def9
.= r1 + (r2 + r3) by Def9
.= (r1 + r2) + r3
.= (addreal . r1,r2) + r3 by Def9
.= addreal . (addreal . r1,r2),r3 by Def9 ; :: thesis: verum