theorem Th7: :: ARYTM_0:7

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