let N be Matrix of n,K; :: thesis: ( N = - M1 implies N is symmetry_circulant )
assume A1: N = - M1 ; :: thesis: N is symmetry_circulant
consider p being FinSequence of K such that
A4: len p = width M1 and
A5: M1 is_symmetry_circulant_about p by Def5;
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 A7: ( width (- M1) = n & len (- p) = len p ) by CARD_1:def 7, MATRIX_1:24;
- M1 is_symmetry_circulant_about - p by A5, T4;
then ex r being FinSequence of K st
( len r = width (- M1) & - M1 is_symmetry_circulant_about r ) by A4, A7, MATRIX_1:24;
hence N is symmetry_circulant by A1, Def5; :: thesis: verum