theorem Th04: :: ANPROJ_9:3

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