theorem :: ARYTM_2:15

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