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
A3:
Seg (len ((- (1_ K)) * p)) = Seg (len p)
by MATRIXR1:16;
A4:
( dom ((- (1_ K)) * p) = Seg (len ((- (1_ K)) * p)) & dom p = Seg (len p) )
by FINSEQ_1:def 3;
A6:
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 )
assume A2:
i in dom p
;
:: thesis: ((- (1_ K)) * p) . i = (- p) . i
A5:
p . i in dom (the multF of K [;] (- (1_ K)),(id the carrier of K))
by A2, A3, A4, FUNCT_1:21;
C1:
p . i in rng p
by A2, FUNCT_1:12;
C2:
rng p c= the
carrier of
K
by FINSEQ_1:def 4;
reconsider b =
p . i as
Element of
K by C1, C2;
C6:
(- (1_ K)) * b = - b
((- (1_ K)) * p) . i =
((- (1_ K)) multfield ) . (p . i)
by A2, FUNCT_1:23
.=
the
multF of
K . (- (1_ K)),
((id the carrier of K) . (p . i))
by A5, FUNCOP_1:42
.=
the
multF of
K . (- (1_ K)),
b
by FUNCT_1:35
.=
(comp K) . b
by C6, VECTSP_1:def 25
.=
(- p) . i
by A2, FUNCT_1:23
;
hence
((- (1_ K)) * p) . i = (- p) . i
;
:: thesis: verum
end;
A7:
p is Element of (len p) -tuples_on the carrier of K
by FINSEQ_2:110;
A8:
- p is Element of (len p) -tuples_on the carrier of K
by A7, FINSEQ_2:133;
A9:
len (- p) = len p
by A8, FINSEQ_1:def 18;
( dom (- p) = Seg (len (- p)) & dom p = Seg (len p) )
by FINSEQ_1:def 3;
hence
(- (1_ K)) * p = - p
by A3, A4, A9, A6, FINSEQ_1:17; :: thesis: verum