let K be Field; :: thesis: for p being FinSequence of K st p is first-line-of-anti-circular holds
- p is first-line-of-anti-circular
let p be FinSequence of K; :: thesis: ( p is first-line-of-anti-circular implies - p is first-line-of-anti-circular )
set n = len p;
assume A1: p is first-line-of-anti-circular ; :: thesis: - p is first-line-of-anti-circular
consider M1 being Matrix of len p,K such that
A2: M1 is_anti-circular_about p by A1, Def12;
set M2 = - M1;
A4: ( Indices M1 = [:(Seg (len p)),(Seg (len p)):] & len M1 = len p & width M1 = len p & Indices (- M1) = [:(Seg (len p)),(Seg (len p)):] & len (- M1) = len p & width (- M1) = len p ) by MATRIX_1:25;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:110;
then A6: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:133;
then A7: ( len (- p) = len p & len p = len p ) by FINSEQ_1:def 18;
then E1: ( dom (- p) = Seg (len p) & dom p = Seg (len p) ) by FINSEQ_1:def 3;
A8: for i, j being Nat st [i,j] in Indices (- M1) & i <= j holds
(- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (- M1) & i <= j implies (- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1) )
assume B1: ( [i,j] in Indices (- M1) & i <= j ) ; :: thesis: (- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1)
((j - i) mod (len p)) + 1 in Seg (len p) by B1, A4, Lm2;
then B23: ((j - i) mod (len p)) + 1 in dom p by FINSEQ_1:def 3;
(- M1) * i,j = - (M1 * i,j) by B1, A4, MATRIX_3:def 2
.= (comp K) . (M1 * i,j) by VECTSP_1:def 25
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by B1, A4, A2, Def10
.= (- p) . (((j - i) mod (len p)) + 1) by B23, FUNCT_1:23 ;
hence (- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1) by A6, FINSEQ_1:def 18; :: thesis: verum

end;

for i, j being Nat st [i,j] in Indices (- M1) & i >= j holds
(- M1) * i,j = (- (- p)) . (((j - i) mod (len (- p))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (- M1) & i >= j implies (- M1) * i,j = (- (- p)) . (((j - i) mod (len (- p))) + 1) )
assume B1: ( [i,j] in Indices (- M1) & i >= j ) ; :: thesis: (- M1) * i,j = (- (- p)) . (((j - i) mod (len (- p))) + 1)
B2: ((j - i) mod (len p)) + 1 in Seg (len p) by B1, A4, Lm2;
(- M1) * i,j = - (M1 * i,j) by B1, A4, MATRIX_3:def 2
.= (comp K) . (M1 * i,j) by VECTSP_1:def 25
.= (comp K) . ((- p) . (((j - i) mod (len p)) + 1)) by B1, A4, A2, Def10
.= (- (- p)) . (((j - i) mod (len p)) + 1) by E1, B2, FUNCT_1:23 ;
hence (- M1) * i,j = (- (- p)) . (((j - i) mod (len (- p))) + 1) by A6, FINSEQ_1:def 18; :: thesis: verum

end;

then A9: - M1 is_anti-circular_about - p by A8, A7, A4, Def10;
consider M2 being Matrix of len (- p),K such that
A10: M2 is_anti-circular_about - p by A9, A7;
take M2 ; :: according to MATRIX16:def 11 :: thesis: M2 is_anti-circular_about - p
thus M2 is_anti-circular_about - p by A10; :: thesis: verum