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

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