for x being Element of REAL+ st x <> {} holds
ex y being Element of REAL+ st x *' y = one