let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for x being real number holds
( not x * p1 = x * p2 or x = 0 or p1 = p2 )
let p1, p2 be Point of (TOP-REAL n); :: thesis: for x being real number holds
( not x * p1 = x * p2 or x = 0 or p1 = p2 )
let x be real number ; :: thesis: ( not x * p1 = x * p2 or x = 0 or p1 = p2 )
assume that
A1: x * p1 = x * p2 and
A2: x <> 0 ; :: thesis: p1 = p2
((1 / x) * x) * p1 = (1 / x) * (x * p2) by A1, RVSUM_1:71;
then ((1 / x) * x) * p1 = ((1 / x) * x) * p2 by RVSUM_1:71;
then 1 * p1 = ((1 / x) * x) * p2 by A2, XCMPLX_1:107;
then 1 * p1 = 1 * p2 by A2, XCMPLX_1:107;
hence p1 = 1 * p2 by RVSUM_1:74
.= p2 by RVSUM_1:74 ;
:: thesis: verum