thus multreal is commutative :: thesis: multreal is associative

proof

let r1, r2 be Element of REAL ; :: according to BINOP_1:def 2 :: thesis: multreal . (r1,r2) = multreal . (r2,r1)
thus multreal . (r1,r2) = r1 * r2 by Def11
.= multreal . (r2,r1) by Def11 ; :: thesis: verum

end;

let r1, r2, r3 be Element of REAL ; :: according to BINOP_1:def 3 :: thesis: multreal . (r1,(multreal . (r2,r3))) = multreal . ((multreal . (r1,r2)),r3)
thus multreal . (r1,(multreal . (r2,r3))) = r1 * (multreal . (r2,r3)) by Def11
.= r1 * (r2 * r3) by Def11
.= (r1 * r2) * r3
.= (multreal . (r1,r2)) * r3 by Def11
.= multreal . ((multreal . (r1,r2)),r3) by Def11 ; :: thesis: verum