theorem Th57: :: ARYTM_3:57

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