let K be Field; :: thesis: for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (- p) = - (CCirc p)
let p be FinSequence of K; :: thesis: ( p is first-col-of-circulant implies CCirc (- p) = - (CCirc p) )
set n = len p;
A1: dom p = Seg (len p) by FINSEQ_1:def 3;
A2: Indices (CCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
assume A3: p is first-col-of-circulant ; :: thesis: CCirc (- p) = - (CCirc p)
then A4: CCirc p is_col_circulant_about p by Def8;
- p is first-col-of-circulant by A3, Th35;
then A5: CCirc (- p) is_col_circulant_about - p by Def8;
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 A6: len (- p) = len p by CARD_1:def 7;
then A7: Indices (CCirc p) = Indices (CCirc (- p)) by MATRIX_0:26;
A8: for i, j being Nat st [i,j] in Indices (CCirc p) holds
(CCirc (- p)) * (i,j) = - ((CCirc p) * (i,j))

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (CCirc p) implies (CCirc (- p)) * (i,j) = - ((CCirc p) * (i,j)) )
assume A9: [i,j] in Indices (CCirc p) ; :: thesis: (CCirc (- p)) * (i,j) = - ((CCirc p) * (i,j))
then A10: ((i - j) mod (len p)) + 1 in Seg (len p) by A2, Lm3;
(CCirc (- p)) * (i,j) = (- p) . (((i - j) mod (len (- p))) + 1) by A5, A7, A9
.= (comp K) . (p . (((i - j) mod (len p)) + 1)) by A6, A1, A10, FUNCT_1:13
.= (comp K) . ((CCirc p) * (i,j)) by A4, A9
.= - ((CCirc p) * (i,j)) by VECTSP_1:def 13 ;
hence (CCirc (- p)) * (i,j) = - ((CCirc p) * (i,j)) ; :: thesis: verum

end;

A11: ( len (CCirc p) = len p & width (CCirc p) = len p ) by MATRIX_0:24;
( len (CCirc (- p)) = len p & width (CCirc (- p)) = len p ) by A6, MATRIX_0:24;
hence CCirc (- p) = - (CCirc p) by A11, A8, MATRIX_3:def 2; :: thesis: verum