let M be Matrix of n,K; :: thesis: ( M = M1 + M2 implies M is symmetry_circulant )
assume A1: M = M1 + M2 ; :: thesis: M is symmetry_circulant
consider p being FinSequence of K such that
A2: len p = width M1 and
A3: M1 is_symmetry_circulant_about p by Def5;
width M1 = n by MATRIX_0:24;
then A4: dom p = Seg n by A2, FINSEQ_1:def 3;
consider q being FinSequence of K such that
A5: len q = width M2 and
A6: M2 is_symmetry_circulant_about q by Def5;
A7: n in NAT by ORDINAL1:def 12;
width M2 = n by MATRIX_0:24;
then dom q = Seg n by A5, FINSEQ_1:def 3;
then dom (p + q) = dom p by A4, POLYNOM1:1;
then A8: len (p + q) = n by A4, A7, FINSEQ_1:def 3;
width (M1 + M2) = n by MATRIX_0:24;
then ex r being FinSequence of K st
( len r = width (M1 + M2) & M1 + M2 is_symmetry_circulant_about r ) by A8, A3, A6, Th5;
hence M is symmetry_circulant by A1; :: thesis: verum