let K be Field; :: thesis: for p, q being FinSequence of K st len p = len q & p is first-line-of-circulant & q is first-line-of-circulant holds
LCirc (p + q) = (LCirc p) + (LCirc q)
let p, q be FinSequence of K; :: thesis: ( len p = len q & p is first-line-of-circulant & q is first-line-of-circulant implies LCirc (p + q) = (LCirc p) + (LCirc q) )
set n = len p;
assume A1: ( len p = len q & p is first-line-of-circulant & q is first-line-of-circulant ) ; :: thesis: LCirc (p + q) = (LCirc p) + (LCirc q)
A2: p + q is first-line-of-circulant by A1, Th33;
A3: ( 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 A4: dom (p + q) = dom p by POLYNOM1:5;
A5: len (p + q) = len p by A3, A4, FINSEQ_1:def 3;
A7: LCirc p is_line_circulant_about p by A1, Def7;
A9: LCirc q is_line_circulant_about q by A1, Def7;
A11: LCirc (p + q) is_line_circulant_about p + q by A2, Def7;
A13: ( len (LCirc (p + q)) = len p & len (LCirc p) = len p & width (LCirc (p + q)) = len p & width (LCirc p) = len p ) by A5, MATRIX_1:25;
A15: ( Indices (LCirc p) = Indices (LCirc (p + q)) & Indices (LCirc p) = Indices (LCirc q) & Indices (LCirc p) = [:(Seg (len p)),(Seg (len p)):] ) by A1, A5, MATRIX_1:25, MATRIX_1:27;
for i, j being Nat st [i,j] in Indices (LCirc p) holds
(LCirc (p + q)) * i,j = ((LCirc p) * i,j) + ((LCirc q) * i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (LCirc p) implies (LCirc (p + q)) * i,j = ((LCirc p) * i,j) + ((LCirc q) * i,j) )
assume B1: [i,j] in Indices (LCirc p) ; :: thesis: (LCirc (p + q)) * i,j = ((LCirc p) * i,j) + ((LCirc q) * i,j)
then B2: ( [i,j] in Indices (LCirc q) & [i,j] in Indices (LCirc (p + q)) & ((j - i) mod (len p)) + 1 in Seg (len p) ) by A15, Lm2;
(LCirc (p + q)) * i,j = (p + q) . (((j - i) mod (len (p + q))) + 1) by A11, Def1, B1, A15
.= the addF of K . (p . (((j - i) mod (len (p + q))) + 1)),(q . (((j - i) mod (len (p + q))) + 1)) by A3, A5, B2, FUNCOP_1:28
.= the addF of K . ((LCirc p) * i,j),(q . (((j - i) mod (len q)) + 1)) by A1, A5, B1, A7, Def1
.= ((LCirc p) * i,j) + ((LCirc q) * i,j) by B1, A15, A9, Def1 ;
hence (LCirc (p + q)) * i,j = ((LCirc p) * i,j) + ((LCirc q) * i,j) ; :: thesis: verum

end;

hence LCirc (p + q) = (LCirc p) + (LCirc q) by A13, MATRIX_3:def 3; :: thesis: verum