let K be Field; :: thesis: for a being Element of K
for x being FinSequence of K holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
let a be Element of K; :: thesis: for x being FinSequence of K holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
let x be FinSequence of K; :: thesis: ( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
set n = len x;
reconsider x0 = x as Element of (len x) -tuples_on the carrier of K by Th1;
reconsider y = a * x0 as Element of (len x) -tuples_on the carrier of K ;
thus - (a * x) = (- (1_ K)) * y by FVSUM_1:59
.= ((- (1_ K)) * a) * x0 by FVSUM_1:54
.= (- ((1_ K) * a)) * x0 by VECTSP_1:8
.= (- a) * x ; :: thesis: - (a * x) = a * (- x)
thus - (a * x) = (- (1_ K)) * y by FVSUM_1:59
.= ((- (1_ K)) * a) * x0 by FVSUM_1:54
.= a * ((- (1_ K)) * x0) by FVSUM_1:54
.= a * (- x) by FVSUM_1:59 ; :: thesis: verum