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 that
A1: p is first-col-of-circulant and
A2: q is first-col-of-circulant and
A3: len p = len q ; :: thesis: p + q is first-col-of-circulant
consider M2 being Matrix of len p,K such that
A4: M2 is_col_circulant_about q by A2, A3;
A5: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def 3;
A6: dom p = Seg (len p) by FINSEQ_1:def 3;
dom q = Seg (len p) by A3, FINSEQ_1:def 3;
then A7: dom (p + q) = dom p by A6, POLYNOM1:1;
then A8: len (p + q) = len p by A6, FINSEQ_1:def 3;
consider M1 being Matrix of len p,K such that
A9: M1 is_col_circulant_about p by A1;
A10: Indices M1 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
set M3 = M1 + M2;
A11: len (M1 + M2) = len p by MATRIX_0:24;
A12: Indices M2 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
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 A13: [i,j] in Indices (M1 + M2) ; :: thesis: (M1 + M2) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1)
then A14: [i,j] in Indices M1 by A10, MATRIX_0:24;
then A15: ((i - j) mod (len (p + q))) + 1 in dom (p + q) by A10, A6, A5, A7, Lm3;
A16: [i,j] in Indices M2 by A12, A13, MATRIX_0:24;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A14, MATRIX_3:def 3
.= the addF of K . ((M1 * (i,j)),(q . (((i - j) mod (len q)) + 1))) by A4, A16
.= the addF of K . ((p . (((i - j) mod (len (p + q))) + 1)),(q . (((i - j) mod (len (p + q))) + 1))) by A3, A9, A8, A14
.= (p + q) . (((i - j) mod (len (p + q))) + 1) by A15, FUNCOP_1:22 ;
hence (M1 + M2) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1) ; :: thesis: verum

end;

then M1 + M2 is_col_circulant_about p + q by A11, A8;
then consider M3 being Matrix of len (p + q),K such that
len (p + q) = len M3 and
A17: M3 is_col_circulant_about p + q by A11;
take M3 ; :: according to MATRIX16:def 6 :: thesis: M3 is_col_circulant_about p + q
thus M3 is_col_circulant_about p + q by A17; :: thesis: verum