let n be Element of NAT ; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is line_circulant holds
- M1 is line_circulant
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is line_circulant holds
- M1 is line_circulant
let M1 be Matrix of n,K; :: thesis: ( M1 is line_circulant implies - M1 is line_circulant )
assume A1: M1 is line_circulant ; :: thesis: - M1 is line_circulant
consider p being FinSequence of K such that
A2: ( len p = width M1 & M1 is_line_circulant_about p ) by A1, Def2;
A4: ( Indices M1 = [:(Seg n),(Seg n):] & len M1 = n & width M1 = n & Indices (- M1) = [:(Seg n),(Seg n):] & len (- M1) = n & width (- M1) = n ) by MATRIX_1:25;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:110;
then E1: - 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;
for i, j being Nat st [i,j] in Indices (- M1) holds
(- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (- M1) implies (- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1) )
assume B1: [i,j] in Indices (- M1) ; :: thesis: (- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1)
((j - i) mod n) + 1 in Seg n by B1, A4, Lm2;
then B23: ((j - i) mod (len p)) + 1 in dom p by A4, A2, 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, Def1
.= (- p) . (((j - i) mod (len p)) + 1) by B23, FUNCT_1:23 ;
hence (- M1) * i,j = (- p) . (((j - i) mod (len (- p))) + 1) by E1, FINSEQ_1:def 18; :: thesis: verum

end;

then A9: - M1 is_line_circulant_about - p by A4, A2, A6, Def1;
set r = - p;
consider r being FinSequence of K such that
A10: ( len r = width (- M1) & - M1 is_line_circulant_about r ) by A4, A2, A6, A9;
take r ; :: according to MATRIX16:def 2 :: thesis: ( len r = width (- M1) & - M1 is_line_circulant_about r )
thus ( len r = width (- M1) & - M1 is_line_circulant_about r ) by A10; :: thesis: verum