let K be Field; :: thesis: for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
ACirc (p + q) = (ACirc p) + (ACirc q)
let p, q be FinSequence of K; :: thesis: ( p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q implies ACirc (p + q) = (ACirc p) + (ACirc q) )
set n = len p;
assume A1: ( p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q ) ; :: thesis: ACirc (p + q) = (ACirc p) + (ACirc q)
A2: p + q is first-line-of-anti-circular by A1, Th60;
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;
A6: ( ACirc p is_anti-circular_about p & ACirc q is_anti-circular_about q ) by A1, Def13;
A7: ( Indices (ACirc p) = [:(Seg (len p)),(Seg (len p)):] & len (ACirc p) = len p & width (ACirc p) = len p & Indices (ACirc q) = [:(Seg (len p)),(Seg (len p)):] & len (ACirc q) = len p & width (ACirc q) = len p ) by A1, MATRIX_1:25;
E1: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:110;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:133;
then D1: len (- p) = len p by FINSEQ_1:def 18;
E2: q is Element of (len q) -tuples_on the carrier of K by FINSEQ_2:110;
then - q is Element of (len q) -tuples_on the carrier of K by FINSEQ_2:133;
then D2: len (- q) = len q by FINSEQ_1:def 18;
A11: ACirc (p + q) is_anti-circular_about p + q by A2, Def13;
A13: ( len (ACirc (p + q)) = len p & len (ACirc p) = len p & width (ACirc (p + q)) = len p & width (ACirc p) = len p ) by A5, MATRIX_1:25;
A15: ( Indices (ACirc p) = Indices (ACirc (p + q)) & Indices (ACirc p) = Indices (ACirc q) ) by A1, A5, MATRIX_1:27;
for i, j being Nat st [i,j] in Indices (ACirc p) holds
(ACirc (p + q)) * i,j = ((ACirc p) * i,j) + ((ACirc q) * i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (ACirc p) implies (ACirc (p + q)) * i,j = ((ACirc p) * i,j) + ((ACirc q) * i,j) )
assume B1: [i,j] in Indices (ACirc p) ; :: thesis: (ACirc (p + q)) * i,j = ((ACirc p) * i,j) + ((ACirc q) * i,j)
B2: ( [i,j] in Indices (ACirc q) & [i,j] in Indices (ACirc (p + q)) & ((j - i) mod (len p)) + 1 in Seg (len p) ) by B1, A7, A5, Lm2, MATRIX_1:27;

now

per cases ( i <= j or i >= j ) ;

case C1: i <= j ; :: thesis: (ACirc (p + q)) * i,j = ((ACirc p) * i,j) + ((ACirc q) * i,j)

(ACirc (p + q)) * i,j = (p + q) . (((j - i) mod (len (p + q))) + 1) by A11, Def10, B1, A15, C1
.= 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 . ((ACirc p) * i,j),(q . (((j - i) mod (len q)) + 1)) by A6, B1, Def10, C1, A5, A1
.= ((ACirc p) * i,j) + ((ACirc q) * i,j) by A6, B1, A15, Def10, C1 ;
hence (ACirc (p + q)) * i,j = ((ACirc p) * i,j) + ((ACirc q) * i,j) ; :: thesis: verum

end;

case C2: i >= j ; :: thesis: (ACirc (p + q)) * i,j = ((ACirc p) * i,j) + ((ACirc q) * i,j)

B2: ( dom (- p) = Seg (len p) & dom p = Seg (len p) & dom (- q) = Seg (len q) & dom q = Seg (len p) ) by A1, D1, D2, FINSEQ_1:def 3;
then B3: dom ((- p) + (- q)) = dom (- p) by A1, POLYNOM1:5;
B23: ( ((j - i) mod (len (p + q))) + 1 in dom p & ((j - i) mod (len (p + q))) + 1 in dom ((- p) + (- q)) & ((j - i) mod (len (p + q))) + 1 in dom (- q) & ((j - i) mod (len (p + q))) + 1 in dom (- p) ) by B2, B3, A1, A3, A4, A7, B1, Lm2;
(ACirc (p + q)) * i,j = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) by A11, Def10, B1, A15, C2
.= ((- p) + (- q)) . (((j - i) mod (len (p + q))) + 1) by A1, E1, E2, FVSUM_1:40
.= the addF of K . ((- p) . (((j - i) mod (len (p + q))) + 1)),((- q) . (((j - i) mod (len (p + q))) + 1)) by B23, FUNCOP_1:28
.= the addF of K . ((ACirc p) * i,j),((- q) . (((j - i) mod (len q)) + 1)) by A6, B1, Def10, C2, A1, A5
.= ((ACirc p) * i,j) + ((ACirc q) * i,j) by C2, A7, B1, A6, Def10 ;
hence (ACirc (p + q)) * i,j = ((ACirc p) * i,j) + ((ACirc q) * i,j) ; :: thesis: verum

end;

end;

end;

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

end;

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