theorem :: ARYTM_2:12

for x, y, z being Element of REAL+ holds x *' (y *' z) = (x *' y) *' z