let K be Field; :: thesis: for p being FinSequence of K st p is first-line-of-anti-circular holds
ACirc (- p) = - (ACirc p)
let p be FinSequence of K; :: thesis: ( p is first-line-of-anti-circular implies ACirc (- p) = - (ACirc p) )
set n = len p;
assume A1: p is first-line-of-anti-circular ; :: thesis: ACirc (- p) = - (ACirc p)
then A4: - p is first-line-of-anti-circular by Th58;
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;
A10: ACirc p is_anti-circular_about p by A1, Def13;
A12: ACirc (- p) is_anti-circular_about - p by A4, Def13;
A13: ( len (ACirc (- p)) = len p & len (ACirc p) = len p & width (ACirc (- p)) = len p & width (ACirc p) = len p ) by A6, MATRIX_1:25;
A15: ( Indices (ACirc p) = Indices (ACirc (- p)) & Indices (ACirc 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 (ACirc p) holds
(ACirc (- p)) * i,j = - ((ACirc p) * i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (ACirc p) implies (ACirc (- p)) * i,j = - ((ACirc p) * i,j) )
assume B1: [i,j] in Indices (ACirc p) ; :: thesis: (ACirc (- p)) * i,j = - ((ACirc p) * i,j)

now

per cases ( i <= j or i >= j ) ;

case C1: i <= j ; :: thesis: (ACirc (- p)) * i,j = - ((ACirc p) * i,j)

B2: [i,j] in Indices (ACirc (- p)) by B1, A6, MATRIX_1:27;
((j - i) mod (len p)) + 1 in Seg (len p) by B1, A15, Lm2;
then B23: ((j - i) mod (len p)) + 1 in dom p by FINSEQ_1:def 3;
(ACirc (- p)) * i,j = (- p) . (((j - i) mod (len (- p))) + 1) by C1, B2, A12, Def10
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A6, B23, FUNCT_1:23
.= (comp K) . ((ACirc p) * i,j) by C1, B1, A10, Def10
.= - ((ACirc p) * i,j) by VECTSP_1:def 25 ;
hence (ACirc (- p)) * i,j = - ((ACirc p) * i,j) ; :: thesis: verum

end;

case C2: i >= j ; :: thesis: (ACirc (- p)) * i,j = - ((ACirc p) * i,j)

B2: [i,j] in Indices (ACirc (- p)) by B1, A6, MATRIX_1:27;
((j - i) mod (len p)) + 1 in Seg (len p) by B1, A15, Lm2;
then B23: ((j - i) mod (len p)) + 1 in dom (- p) by A6, FINSEQ_1:def 3;
(ACirc (- p)) * i,j = (- (- p)) . (((j - i) mod (len (- p))) + 1) by C2, B2, A12, Def10
.= (comp K) . ((- p) . (((j - i) mod (len p)) + 1)) by A6, B23, FUNCT_1:23
.= (comp K) . ((ACirc p) * i,j) by C2, B1, A10, Def10
.= - ((ACirc p) * i,j) by VECTSP_1:def 25 ;
hence (ACirc (- p)) * i,j = - ((ACirc p) * i,j) ; :: thesis: verum

end;

end;

end;

hence (ACirc (- p)) * i,j = - ((ACirc p) * i,j) ; :: thesis: verum

end;

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