let n be Element of NAT ; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
M1 + M2 is col_circulant
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
M1 + M2 is col_circulant
let M1, M2 be Matrix of n,K; :: thesis: ( M1 is col_circulant & M2 is col_circulant implies M1 + M2 is col_circulant )
assume that
A1: M1 is col_circulant and
A2: M2 is col_circulant ; :: thesis: M1 + M2 is col_circulant
consider p being FinSequence of K such that
A3: len p = len M1 and
A4: M1 is_col_circulant_about p by A1;
A5: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_0:24;
A6: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_0:24;
consider q being FinSequence of K such that
A7: len q = len M2 and
A8: M2 is_col_circulant_about q by A2;
A9: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_0:24;
A10: len (M1 + M2) = n by MATRIX_0:24;
A11: len M1 = n by MATRIX_0:24;
then A12: dom p = Seg n by A3, FINSEQ_1:def 3;
A13: len M2 = n by MATRIX_0:24;
then dom q = Seg n by A7, FINSEQ_1:def 3;
then A14: dom (p + q) = dom p by A12, POLYNOM1:1;
then A15: len (p + q) = n by A12, FINSEQ_1:def 3;
A16: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def 3;
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 A17: [i,j] in Indices (M1 + M2) ; :: thesis: (M1 + M2) * (i,j) = (p + q) . (((i - j) mod (len (p + q))) + 1)
then A18: ((i - j) mod (len (p + q))) + 1 in Seg n by A6, A12, A16, A14, Lm3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A9, A6, A17, MATRIX_3:def 3
.= the addF of K . ((M1 * (i,j)),(q . (((i - j) mod (len q)) + 1))) by A8, A5, A6, A17
.= the addF of K . ((p . (((i - j) mod (len (p + q))) + 1)),(q . (((i - j) mod (len (p + q))) + 1))) by A4, A7, A9, A11, A13, A6, A15, A17
.= (p + q) . (((i - j) mod (len (p + q))) + 1) by A12, A14, A18, 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 A10, A15;
then consider r being FinSequence of K such that
A19: ( len r = len (M1 + M2) & M1 + M2 is_col_circulant_about r ) ;
take r ; :: according to MATRIX16:def 5 :: thesis: ( len r = len (M1 + M2) & M1 + M2 is_col_circulant_about r )
thus ( len r = len (M1 + M2) & M1 + M2 is_col_circulant_about r ) by A19; :: thesis: verum