let a be Real; :: thesis: for n being Nat

for x1, x2 being Element of REAL n holds

( not a * x1 = a * x2 or a = 0 or x1 = x2 )

let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds

( not a * x1 = a * x2 or a = 0 or x1 = x2 )

let x1, x2 be Element of REAL n; :: thesis: ( not a * x1 = a * x2 or a = 0 or x1 = x2 )

assume that

A1: a * x1 = a * x2 and

A2: a <> 0 ; :: thesis: x1 = x2

((1 / a) * a) * x1 = (1 / a) * (a * x2) by A1, RVSUM_1:49;

then ((1 / a) * a) * x1 = ((1 / a) * a) * x2 by RVSUM_1:49;

then 1 * x1 = ((1 / a) * a) * x2 by A2, XCMPLX_1:106;

then 1 * x1 = 1 * x2 by A2, XCMPLX_1:106;

hence x1 = 1 * x2 by Th3

.= x2 by Th3 ;

:: thesis: verum

for x1, x2 being Element of REAL n holds

( not a * x1 = a * x2 or a = 0 or x1 = x2 )

let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds

( not a * x1 = a * x2 or a = 0 or x1 = x2 )

let x1, x2 be Element of REAL n; :: thesis: ( not a * x1 = a * x2 or a = 0 or x1 = x2 )

assume that

A1: a * x1 = a * x2 and

A2: a <> 0 ; :: thesis: x1 = x2

((1 / a) * a) * x1 = (1 / a) * (a * x2) by A1, RVSUM_1:49;

then ((1 / a) * a) * x1 = ((1 / a) * a) * x2 by RVSUM_1:49;

then 1 * x1 = ((1 / a) * a) * x2 by A2, XCMPLX_1:106;

then 1 * x1 = 1 * x2 by A2, XCMPLX_1:106;

hence x1 = 1 * x2 by Th3

.= x2 by Th3 ;

:: thesis: verum