theorem Th13: :: ARYTM_0:13

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