theorem Th4: :: ARYTM_2:4

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