for x being Element of REAL 0 holds x = <*> REAL ;