for x being Element of REAL holds * (x,x) in REAL+