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

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