let a be Real; :: thesis: for n being Nat
for x being Element of REAL n holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
let n be Nat; :: thesis: for x being Element of REAL n holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
let x be Element of REAL n; :: thesis: ( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
reconsider p = x as Point of (TOP-REAL n) by EUCLID:22;
reconsider x9 = p as Element of n -tuples_on REAL ;
thus - (a * x) = ((- 1) * a) * x9 by RVSUM_1:49
.= (- a) * x ; :: thesis: - (a * x) = a * (- x)
hence - (a * x) = (a * (- 1)) * x
.= a * (- x) by RVSUM_1:49 ;
:: thesis: verum