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 that
A1: a * x = 0* n and
A2: a <> 0 ; :: thesis: x = 0* n
thus x = 1 * x by Th3
.= ((1 / a) * a) * x by A2, XCMPLX_1:106
.= (1 / a) * (a * x) by RVSUM_1:49
.= 0* n by A1, Th2 ; :: thesis: verum