let r be Real; :: thesis: for u being Element of (TOP-REAL 3) st r <> 0 & not u is zero holds
not r * u is zero
let u be Element of (TOP-REAL 3); :: thesis: ( r <> 0 & not u is zero implies not r * u is zero )
assume that
A1: r <> 0 and
A2: not u is zero ; :: thesis: not r * u is zero
r * u <> 0. (TOP-REAL 3)

proof

assume A3: r * u = 0. (TOP-REAL 3) ; :: thesis: contradiction
u = 1 * u by RVSUM_1:52
.= ((1 / r) * r) * u by A1, XCMPLX_1:87
.= (1 / r) * (0. (TOP-REAL 3)) by A3, RVSUM_1:49
.= 0. (TOP-REAL 3) ;
hence contradiction by A2; :: thesis: verum

end;

hence not r * u is zero ; :: thesis: verum