let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is symmetry_circulant holds
M1 @ = M1
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is symmetry_circulant holds
M1 @ = M1
let M1 be Matrix of n,K; :: thesis: ( M1 is symmetry_circulant implies M1 @ = M1 )
assume M1 is symmetry_circulant ; :: thesis: M1 @ = M1
then consider p being FinSequence of K such that
len p = width M1 and
A1: M1 is_symmetry_circulant_about p ;
A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_0:24;
A3: ( len M1 = n & width M1 = n ) by MATRIX_0:24;
A4: ( len (M1 @) = n & width (M1 @) = n ) by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices M1 holds
(M1 @) * (i,j) = M1 * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies (M1 @) * (i,j) = M1 * (i,j) )
assume A5: [i,j] in Indices M1 ; :: thesis: (M1 @) * (i,j) = M1 * (i,j)

per cases ( i + j <> (len p) + 1 or i + j = (len p) + 1 ) ;

suppose A6: i + j <> (len p) + 1 ; :: thesis: (M1 @) * (i,j) = M1 * (i,j)

( i in Seg n & j in Seg n ) by A2, A5, ZFMISC_1:87;
then A7: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
then (M1 @) * (i,j) = M1 * (j,i) by A2, MATRIX_0:def 6
.= p . (((i + j) - 1) mod (len p)) by A1, A7, A6, A2 ;
hence (M1 @) * (i,j) = M1 * (i,j) by A1, A5, A6; :: thesis: verum

end;

suppose A8: i + j = (len p) + 1 ; :: thesis: (M1 @) * (i,j) = M1 * (i,j)

( i in Seg n & j in Seg n ) by A5, A2, ZFMISC_1:87;
then A9: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87;
(M1 @) * (i,j) = M1 * (j,i) by A2, A9, MATRIX_0:def 6
.= p . (len p) by A1, A9, A8, A2 ;
hence (M1 @) * (i,j) = M1 * (i,j) by A1, A8, A5; :: thesis: verum

end;

end;

end;

hence M1 @ = M1 by A3, A4, MATRIX_0:21; :: thesis: verum