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;
A1: ( len (ACirc p) = len p & width (ACirc p) = len p ) by MATRIX_0:24;
A2: Indices (ACirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
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 A3: len (- p) = len p by CARD_1:def 7;
assume A4: p is first-line-of-anti-circular ; :: thesis: ACirc (- p) = - (ACirc p)
then - p is first-line-of-anti-circular by Th58;
then A5: ACirc (- p) is_anti-circular_about - p by Def12;
A6: ACirc p is_anti-circular_about p by A4, Def12;
A7: 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 A8: [i,j] in Indices (ACirc p) ; :: thesis: (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j))

now :: thesis: ( ( i <= j & (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j)) ) or ( i >= j & (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j)) ) )

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

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

((j - i) mod (len p)) + 1 in Seg (len p) by A2, A8, Lm3;
then A10: ((j - i) mod (len p)) + 1 in dom p by FINSEQ_1:def 3;
[i,j] in Indices (ACirc (- p)) by A3, A8, MATRIX_0:26;
then (ACirc (- p)) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) by A5, A9
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A3, A10, FUNCT_1:13
.= (comp K) . ((ACirc p) * (i,j)) by A6, A8, A9
.= - ((ACirc p) * (i,j)) by VECTSP_1:def 13 ;
hence (ACirc (- p)) * (i,j) = - ((ACirc p) * (i,j)) ; :: thesis: verum

end;

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

((j - i) mod (len p)) + 1 in Seg (len p) by A2, A8, Lm3;
then A12: ((j - i) mod (len p)) + 1 in dom (- p) by A3, FINSEQ_1:def 3;
[i,j] in Indices (ACirc (- p)) by A3, A8, MATRIX_0:26;
then (ACirc (- p)) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1) by A5, A11
.= (comp K) . ((- p) . (((j - i) mod (len p)) + 1)) by A3, A12, FUNCT_1:13
.= (comp K) . ((ACirc p) * (i,j)) by A6, A8, A11
.= - ((ACirc p) * (i,j)) by VECTSP_1:def 13 ;
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;

( len (ACirc (- p)) = len p & width (ACirc (- p)) = len p ) by A3, MATRIX_0:24;
hence ACirc (- p) = - (ACirc p) by A1, A7, MATRIX_3:def 2; :: thesis: verum