theorem :: EUCLID_7:4

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