theorem Th56: :: ARYTM_3:56

for x, y, z being Element of RAT+ st x <> {} & x *' y = x *' z holds
y = z