let K be Field; :: thesis: for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds

p + q is first-symmetry-of-circulant

let p, q be FinSequence of K; :: thesis: ( p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q implies p + q is first-symmetry-of-circulant )

set n = len p;

assume that

A1: p is first-symmetry-of-circulant and

A2: q is first-symmetry-of-circulant and

A3: len p = len q ; :: thesis: p + q is first-symmetry-of-circulant

consider M2 being Matrix of len p,K such that

A4: M2 is_symmetry_circulant_about q by A2, A3;

A5: dom p = Seg (len p) by FINSEQ_1:def 3;

dom q = Seg (len p) by A3, FINSEQ_1:def 3;

then dom (p + q) = dom p by A5, POLYNOM1:1;

then A6: len (p + q) = len p by A5, FINSEQ_1:def 3;

consider M1 being Matrix of len p,K such that

A7: M1 is_symmetry_circulant_about p by A1;

width (M1 + M2) = len p by MATRIX_0:24;

then consider M3 being Matrix of len (p + q),K such that

len (p + q) = width M3 and

A8: M3 is_symmetry_circulant_about p + q by A6, A4, A7, Th5;

take M3 ; :: according to MATRIX17:def 6 :: thesis: M3 is_symmetry_circulant_about p + q

thus M3 is_symmetry_circulant_about p + q by A8; :: thesis: verum

p + q is first-symmetry-of-circulant

let p, q be FinSequence of K; :: thesis: ( p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q implies p + q is first-symmetry-of-circulant )

set n = len p;

assume that

A1: p is first-symmetry-of-circulant and

A2: q is first-symmetry-of-circulant and

A3: len p = len q ; :: thesis: p + q is first-symmetry-of-circulant

consider M2 being Matrix of len p,K such that

A4: M2 is_symmetry_circulant_about q by A2, A3;

A5: dom p = Seg (len p) by FINSEQ_1:def 3;

dom q = Seg (len p) by A3, FINSEQ_1:def 3;

then dom (p + q) = dom p by A5, POLYNOM1:1;

then A6: len (p + q) = len p by A5, FINSEQ_1:def 3;

consider M1 being Matrix of len p,K such that

A7: M1 is_symmetry_circulant_about p by A1;

width (M1 + M2) = len p by MATRIX_0:24;

then consider M3 being Matrix of len (p + q),K such that

len (p + q) = width M3 and

A8: M3 is_symmetry_circulant_about p + q by A6, A4, A7, Th5;

take M3 ; :: according to MATRIX17:def 6 :: thesis: M3 is_symmetry_circulant_about p + q

thus M3 is_symmetry_circulant_about p + q by A8; :: thesis: verum