theorem Th4: :: XCMPLX_1:4

for a, b, c being Complex holds a * (b * c) = (a * b) * c ;