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

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