let K be Field; :: thesis: for p, q being FinSequence of K st len p = len q & p is first-symmetry-of-circulant & q is first-symmetry-of-circulant holds
SCirc (p + q) = (SCirc p) + (SCirc q)
let p, q be FinSequence of K; :: thesis: ( len p = len q & p is first-symmetry-of-circulant & q is first-symmetry-of-circulant implies SCirc (p + q) = (SCirc p) + (SCirc q) )
set n = len p;
assume that
A1: len p = len q and
A2: p is first-symmetry-of-circulant and
A3: q is first-symmetry-of-circulant ; :: thesis: SCirc (p + q) = (SCirc p) + (SCirc q)
A4: ( SCirc q is_symmetry_circulant_about q & Indices (SCirc p) = Indices (SCirc q) ) by A1, A3, Def7, MATRIX_0:26;
p + q is first-symmetry-of-circulant by A1, A2, A3, Th10;
then A5: SCirc (p + q) is_symmetry_circulant_about p + q by Def7;
A6: dom p = Seg (len p) by FINSEQ_1:def 3;
A7: SCirc p is_symmetry_circulant_about p by A2, Def7;
A8: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def 3;
A9: Indices (SCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
dom q = Seg (len p) by A1, FINSEQ_1:def 3;
then dom (p + q) = dom p by A6, POLYNOM1:1;
then A10: len (p + q) = len p by A6, FINSEQ_1:def 3;
then A11: Indices (SCirc p) = Indices (SCirc (p + q)) by MATRIX_0:26;
A12: for i, j being Nat st [i,j] in Indices (SCirc p) holds
(SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (SCirc p) implies (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) )
assume A13: [i,j] in Indices (SCirc p) ; :: thesis: (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))

now :: thesis: (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))

per cases ( i + j <> (len (p + q)) + 1 or i + j = (len (p + q)) + 1 ) ;

suppose A14: i + j <> (len (p + q)) + 1 ; :: thesis: (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))

A15: ((i + j) - 1) mod (len p) in Seg (len p) by A9, A13, A14, A10, Lm4;
(SCirc (p + q)) * (i,j) = (p + q) . (((i + j) - 1) mod (len (p + q))) by A5, A11, A13, A14
.= the addF of K . ((p . (((i + j) - 1) mod (len (p + q)))),(q . (((i + j) - 1) mod (len (p + q))))) by A8, A10, A15, FUNCOP_1:22
.= the addF of K . (((SCirc p) * (i,j)),(q . (((i + j) - 1) mod (len q)))) by A1, A10, A7, A13, A14
.= ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) by A1, A4, A13, A14, A10 ;
hence (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) ; :: thesis: verum

end;

suppose A16: i + j = (len (p + q)) + 1 ; :: thesis: (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j))

( i in Seg (len p) & j in Seg (len p) ) by A9, A13, ZFMISC_1:87;
then ( 1 <= i & 1 <= j ) by FINSEQ_1:1;
then 1 + 1 <= i + j by XREAL_1:7;
then ((len (p + q)) + 1) - 1 >= (1 + 1) - 1 by A16, XREAL_1:9;
then len (p + q) in Seg (len (p + q)) ;
then A17: len (p + q) in dom (p + q) by FINSEQ_1:def 3;
(SCirc (p + q)) * (i,j) = (p + q) . (len (p + q)) by A5, A11, A13, A16
.= the addF of K . ((p . (len (p + q))),(q . (len (p + q)))) by A17, FUNCOP_1:22
.= the addF of K . (((SCirc p) * (i,j)),(q . (len q))) by A1, A10, A7, A13, A16
.= ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) by A4, A13, A16, A1, A10 ;
hence (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) ; :: thesis: verum

end;

end;

end;

hence (SCirc (p + q)) * (i,j) = ((SCirc p) * (i,j)) + ((SCirc q) * (i,j)) ; :: thesis: verum

end;

A18: ( len (SCirc p) = len p & width (SCirc p) = len p ) by MATRIX_0:24;
( len (SCirc (p + q)) = len p & width (SCirc (p + q)) = len p ) by A10, MATRIX_0:24;
hence SCirc (p + q) = (SCirc p) + (SCirc q) by A18, A12, MATRIX_3:def 3; :: thesis: verum