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: b * c = q * r by BINOP_2:def 11;
a * b = p * q by BINOP_2:def 11;
hence (a * b) * c = (p * q) * r by BINOP_2:def 11
.= p * (q * r)
.= a * (b * c) by A1, BINOP_2:def 11 ;
:: thesis: verum