thus addreal is commutative :: thesis: addreal is associative

proof

let r1, r2 be Element of REAL ; :: according to BINOP_1:def 2 :: 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, r2, r3 be Element of REAL ; :: according to BINOP_1:def 3 :: 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