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
len p = width M1 and
A2: M1 is_symmetry_circulant_about p by Def5;
- M1 is_symmetry_circulant_about - p by A2, Th4;
then ex r being FinSequence of K st
( len r = width (- M1) & - M1 is_symmetry_circulant_about r ) ;
hence N is symmetry_circulant by A1; :: thesis: verum