theorem Th66: :: XXREAL_3:66
for x, y, z being ExtReal holds x * (y * z) = (x * y) * z