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) )
thus - (a * x) = ((- 1) * a) * x by EUCLID_4:4
.= (- a) * x ; :: thesis: - (a * x) = a * (- x)
hence - (a * x) = (a * (- 1)) * x
.= a * (- x) by EUCLID_4:4 ;
:: thesis: verum