let a be Real; :: thesis: for n being Nat
for x being Element of REAL n holds
( not a * x = 0* n or a = 0 or x = 0* n )
let n be Nat; :: thesis: for x being Element of REAL n holds
( not a * x = 0* n or a = 0 or x = 0* n )
let x be Element of REAL n; :: thesis: ( not a * x = 0* n or a = 0 or x = 0* n )
assume A1: ( a * x = 0* n & a <> 0 ) ; :: thesis: x = 0* n
thus x = 1 * x by Th3
.= ((1 / a) * a) * x by A1, XCMPLX_1:107
.= (1 / a) * (a * x) by RVSUM_1:71
.= 0* n by A1, Th2 ; :: thesis: verum