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 BB100;
reconsider x1 = x as Element of (len x) -tuples_on the carrier of K by BB100;
reconsider y = a * x0 as Element of (len x) -tuples_on the carrier of K ;
thus - (a * x) = (- (1_ K)) * y by FVSUM_1:72
.= ((- (1_ K)) * a) * x0 by FVSUM_1:67
.= (- ((1_ K) * a)) * x0 by VECTSP_1:40
.= (- a) * x by VECTSP_1:def 19 ; :: thesis: - (a * x) = a * (- x)
thus - (a * x) = (- (1_ K)) * y by FVSUM_1:72
.= ((- (1_ K)) * a) * x0 by FVSUM_1:67
.= a * ((- (1_ K)) * x0) by FVSUM_1:67
.= a * (- x) by FVSUM_1:72 ; :: thesis: verum