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_1:24;
then A7: dom p = Seg n by A2, FINSEQ_1:def 3;
consider q being FinSequence of K such that
A8: len q = width M2 and
A9: M2 is_symmetry_circulant_about q by Def5;
A11: n in NAT by ORDINAL1:def 12;
width M2 = n by MATRIX_1:24;
then dom q = Seg n by A8, FINSEQ_1:def 3;
then dom (p + q) = dom p by A7, POLYNOM1:1;
then A14: len (p + q) = n by A7, A11, FINSEQ_1:def 3;
width (M1 + M2) = n by MATRIX_1:24;
then ex r being FinSequence of K st
( len r = width (M1 + M2) & M1 + M2 is_symmetry_circulant_about r ) by A14, A3, A9, T3;
hence M is symmetry_circulant by A1, Def5; :: thesis: verum