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

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