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 A1: ( M1 is col_circulant & M2 is col_circulant ) ; :: thesis: M1 + M2 is col_circulant
consider p being FinSequence of K such that
A2: ( len p = len M1 & M1 is_col_circulant_about p ) by A1, Def5;
consider q being FinSequence of K such that
A3: ( len q = len M2 & M2 is_col_circulant_about q ) by A1, Def5;
A6: ( Indices M1 = [:(Seg n),(Seg n):] & len M1 = n & width M1 = n & Indices M2 = [:(Seg n),(Seg n):] & len M2 = n & width M2 = n & Indices (M1 + M2) = [:(Seg n),(Seg n):] & len (M1 + M2) = n & width (M1 + M2) = n ) by MATRIX_1:25;
A8: ( dom p = Seg n & dom (p + q) = Seg (len (p + q)) & dom p = Seg (len p) & dom q = Seg n ) by A2, A3, A6, FINSEQ_1:def 3;
then A9: dom (p + q) = dom p by POLYNOM1:5;
then A10: len (p + q) = n by A8, 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 B1: [i,j] in Indices (M1 + M2) ; :: thesis: (M1 + M2) * i,j = (p + q) . (((i - j) mod (len (p + q))) + 1)
then B3: ((i - j) mod (len (p + q))) + 1 in Seg n by A9, A8, A6, Lm2;
(M1 + M2) * i,j = (M1 * i,j) + (M2 * i,j) by B1, A6, MATRIX_3:def 3
.= the addF of K . (M1 * i,j),(q . (((i - j) mod (len q)) + 1)) by B1, A6, A3, Def4
.= the addF of K . (p . (((i - j) mod (len (p + q))) + 1)),(q . (((i - j) mod (len (p + q))) + 1)) by B1, A6, A2, Def4, A3, A10
.= (p + q) . (((i - j) mod (len (p + q))) + 1) by B3, A8, A9, FUNCOP_1:28 ;
hence (M1 + M2) * i,j = (p + q) . (((i - j) mod (len (p + q))) + 1) ; :: thesis: verum

end;

then A9: M1 + M2 is_col_circulant_about p + q by A6, A10, Def4;
set r = p + q;
consider r being FinSequence of K such that
A11: ( len r = len (M1 + M2) & M1 + M2 is_col_circulant_about r ) by A6, A9, A10;
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 A11; :: thesis: verum