let K be Field; :: thesis: for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds
p + q is first-col-of-circulant
let p, q be FinSequence of K; :: thesis: ( p is first-col-of-circulant & q is first-col-of-circulant & len p = len q implies p + q is first-col-of-circulant )
set n = len p;
assume A1: ( p is first-col-of-circulant & q is first-col-of-circulant & len p = len q ) ; :: thesis: p + q is first-col-of-circulant
consider M1 being Matrix of len p,K such that
A2: M1 is_col_circulant_about p by A1, Def6;
consider M2 being Matrix of len p,K such that
A4: M2 is_col_circulant_about q by A1, Def6;
A6: ( Indices M1 = [:(Seg (len p)),(Seg (len p)):] & len M1 = len p & width M1 = len p & Indices M2 = [:(Seg (len p)),(Seg (len p)):] & len M2 = len p & width M2 = len p ) by MATRIX_1:25;
A7: ( len q = len p & len p = len p & len (M1 + M2) = len p & width (M1 + M2) = len p ) by A1, MATRIX_1:25;
A8: ( dom p = Seg (len p) & dom (p + q) = Seg (len (p + q)) & dom p = Seg (len p) & dom q = Seg (len p) ) by A1, FINSEQ_1:def 3;
then A9: dom (p + q) = dom p by POLYNOM1:5;
A10: len (p + q) = len p by A8, A9, FINSEQ_1:def 3;
set M3 = M1 + M2;
A12: for i, j being Nat st [i,j] in Indices (M1 + M2) holds
(M1 + M2) * i,j = (p + q) . (((i - j) mod (len (p + q))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (M1 + M2) implies (M1 + M2) * i,j = (p + q) . (((i - j) mod (len (p + q))) + 1) )
assume [i,j] in Indices (M1 + M2) ; :: thesis: (M1 + M2) * i,j = (p + q) . (((i - j) mod (len (p + q))) + 1)
then B2: ( [i,j] in Indices M1 & [i,j] in Indices M2 ) by A6, MATRIX_1:25;
then B23: ( ((i - j) mod (len (p + q))) + 1 in dom p & ((i - j) mod (len (p + q))) + 1 in dom (p + q) & ((i - j) mod (len (p + q))) + 1 in dom q ) by A8, A9, A6, Lm2;
(M1 + M2) * i,j = (M1 * i,j) + (M2 * i,j) by B2, MATRIX_3:def 3
.= the addF of K . (M1 * i,j),(q . (((i - j) mod (len q)) + 1)) by B2, A4, Def4
.= the addF of K . (p . (((i - j) mod (len (p + q))) + 1)),(q . (((i - j) mod (len (p + q))) + 1)) by B2, A2, Def4, A1, A10
.= (p + q) . (((i - j) mod (len (p + q))) + 1) by B23, FUNCOP_1:28 ;
hence (M1 + M2) * i,j = (p + q) . (((i - j) mod (len (p + q))) + 1) ; :: thesis: verum

end;

A13: M1 + M2 is_col_circulant_about p + q by A7, Def4, A10, A12;
consider M3 being Matrix of len (p + q),K such that
A14: ( len (p + q) = len M3 & M3 is_col_circulant_about p + q ) by A7, A10, A13;
take M3 ; :: according to MATRIX16:def 6 :: thesis: M3 is_col_circulant_about p + q
thus M3 is_col_circulant_about p + q by A14; :: thesis: verum