thus multreal is commutative :: thesis: multreal is associative

proof

let r1 be Element of REAL ; :: according to BINOP_1:def 13 :: thesis: for b₁ being Element of REAL holds multreal . r1,b₁ = multreal . b₁,r1
let r2 be Element of REAL ; :: 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 be Element of REAL ; :: according to BINOP_1:def 14 :: thesis: for b₁, b₂ being Element of REAL holds multreal . r1,(multreal . b₁,b₂) = multreal . (multreal . r1,b₁),b₂
let r2, r3 be Element of REAL ; :: 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