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 p is first-line-of-anti-circular ; :: thesis: - p is first-line-of-anti-circular
then consider M1 being Matrix of len p,K such that
A1: M1 is_anti-circular_about p ;
set M2 = - M1;
A2: Indices M1 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
A3: Indices (- M1) = [:(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 A4: - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A5: len (- p) = len p by CARD_1:def 7;
then A6: dom (- p) = Seg (len p) by FINSEQ_1:def 3;
A7: 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 that
A8: [i,j] in Indices (- M1) and
A9: i >= j ; :: thesis: (- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1)
A10: ((j - i) mod (len p)) + 1 in Seg (len p) by A3, A8, Lm3;
(- M1) * (i,j) = - (M1 * (i,j)) by A2, A3, A8, MATRIX_3:def 2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def 13
.= (comp K) . ((- p) . (((j - i) mod (len p)) + 1)) by A1, A2, A3, A8, A9
.= (- (- p)) . (((j - i) mod (len p)) + 1) by A6, A10, FUNCT_1:13 ;
hence (- M1) * (i,j) = (- (- p)) . (((j - i) mod (len (- p))) + 1) by A4, CARD_1:def 7; :: thesis: verum

end;

A11: 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 that
A12: [i,j] in Indices (- M1) and
A13: i <= j ; :: thesis: (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1)
((j - i) mod (len p)) + 1 in Seg (len p) by A3, A12, Lm3;
then A14: ((j - i) mod (len p)) + 1 in dom p by FINSEQ_1:def 3;
(- M1) * (i,j) = - (M1 * (i,j)) by A2, A3, A12, MATRIX_3:def 2
.= (comp K) . (M1 * (i,j)) by VECTSP_1:def 13
.= (comp K) . (p . (((j - i) mod (len p)) + 1)) by A1, A2, A3, A12, A13
.= (- p) . (((j - i) mod (len p)) + 1) by A14, FUNCT_1:13 ;
hence (- M1) * (i,j) = (- p) . (((j - i) mod (len (- p))) + 1) by A4, CARD_1:def 7; :: thesis: verum

end;

width (- M1) = len p by MATRIX_0:24;
then - M1 is_anti-circular_about - p by A5, A11, A7;
then consider M2 being Matrix of len (- p),K such that
A15: M2 is_anti-circular_about - p by A5;
take M2 ; :: according to MATRIX16:def 11 :: thesis: M2 is_anti-circular_about - p
thus M2 is_anti-circular_about - p by A15; :: thesis: verum