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;
assume A1: p is first-col-of-circulant ; :: thesis: CCirc (- p) = - (CCirc p)
A4: - p is first-col-of-circulant by A1, Th35;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:110;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:133;
then A6: len (- p) = len p by FINSEQ_1:def 18;
A7: ( dom (- p) = Seg (len (- p)) & dom p = Seg (len p) ) by FINSEQ_1:def 3;
A10: CCirc p is_col_circulant_about p by A1, Def8;
A12: CCirc (- p) is_col_circulant_about - p by A4, Def8;
A13: ( len (CCirc (- p)) = len p & len (CCirc p) = len p & width (CCirc (- p)) = len p & width (CCirc p) = len p ) by A6, MATRIX_1:25;
A15: ( Indices (CCirc p) = Indices (CCirc (- p)) & Indices (CCirc p) = [:(Seg (len p)),(Seg (len p)):] ) by A6, MATRIX_1:25, MATRIX_1:27;
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 B1: [i,j] in Indices (CCirc p) ; :: thesis: (CCirc (- p)) * i,j = - ((CCirc p) * i,j)
then B2: ( [i,j] in Indices (CCirc (- p)) & ((i - j) mod (len p)) + 1 in Seg (len p) ) by A15, Lm2;
(CCirc (- p)) * i,j = (- p) . (((i - j) mod (len (- p))) + 1) by B1, A15, A12, Def4
.= (comp K) . (p . (((i - j) mod (len p)) + 1)) by A6, B2, A7, FUNCT_1:23
.= (comp K) . ((CCirc p) * i,j) by B1, A10, Def4
.= - ((CCirc p) * i,j) by VECTSP_1:def 25 ;
hence (CCirc (- p)) * i,j = - ((CCirc p) * i,j) ; :: thesis: verum

end;

hence CCirc (- p) = - (CCirc p) by A13, MATRIX_3:def 2; :: thesis: verum