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)

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

hence
not r * u is zero
; :: thesis: verum
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;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