for r being Real
for u being Element of (TOP-REAL 3) st r <> 0 & not u is zero holds
not r * u is zero