let a, b, c be Element of multEX_0 ; :: thesis: (a * b) * c = a * (b * c)
reconsider p = a, q = b, r = c as Real ;
A1: a * b = p * q by BINOP_2:def 11;
A2: b * c = q * r by BINOP_2:def 11;
thus (a * b) * c = (p * q) * r by A1, BINOP_2:def 11
.= p * (q * r)
.= a * (b * c) by A2, BINOP_2:def 11 ; :: thesis: verum