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