let K be Field; :: thesis: for p being FinSequence of K holds (- (1_ K)) * p = - p
let p be FinSequence of K; :: thesis: (- (1_ K)) * p = - p
A1: ( Seg (len ((- (1_ K)) * p)) = Seg (len p) & dom ((- (1_ K)) * p) = Seg (len ((- (1_ K)) * p)) ) by FINSEQ_1:def 3, MATRIXR1:16;
A2: dom p = Seg (len p) by FINSEQ_1:def 3;
A3: for i being Nat st i in dom p holds
((- (1_ K)) * p) . i = (- p) . i

proof

let i be Nat; :: thesis: ( i in dom p implies ((- (1_ K)) * p) . i = (- p) . i )
A4: rng p c= the carrier of K by FINSEQ_1:def 4;
assume A5: i in dom p ; :: thesis: ((- (1_ K)) * p) . i = (- p) . i
then A6: p . i in dom ( the multF of K [;] ((- (1_ K)),(id the carrier of K))) by A1, A2, FUNCT_1:11;
p . i in rng p by A5, FUNCT_1:3;
then reconsider b = p . i as Element of K by A4;
((- (1_ K)) * b) + b = ((- (1_ K)) * b) + ((1_ K) * b)
.= ((- (1_ K)) + (1_ K)) * b by VECTSP_1:def 7
.= (0. K) * b by RLVECT_1:5
.= 0. K ;
then ((- (1_ K)) * b) + (b + (- b)) = (0. K) + (- b) by RLVECT_1:def 3;
then (0. K) + (- b) = ((- (1_ K)) * b) + (0. K) by RLVECT_1:5
.= (- (1_ K)) * b by RLVECT_1:4 ;
then A7: (- (1_ K)) * b = - b by RLVECT_1:4;
((- (1_ K)) * p) . i = ((- (1_ K)) multfield) . (p . i) by A5, FUNCT_1:13
.= the multF of K . ((- (1_ K)),((id the carrier of K) . (p . i))) by A6, FUNCOP_1:32
.= the multF of K . ((- (1_ K)),b)
.= (comp K) . b by A7, VECTSP_1:def 13
.= (- p) . i by A5, FUNCT_1:13 ;
hence ((- (1_ K)) * p) . i = (- p) . i ; :: thesis: verum

end;

p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A8: len (- p) = len p by CARD_1:def 7;
( dom (- p) = Seg (len (- p)) & dom p = Seg (len p) ) by FINSEQ_1:def 3;
hence (- (1_ K)) * p = - p by A1, A3, A8, FINSEQ_1:13; :: thesis: verum