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 that
A1: p is first-line-of-anti-circular and
A2: q is first-line-of-anti-circular and
A3: len p = len q ; :: thesis: ACirc (p + q) = (ACirc p) + (ACirc q)
A4: dom p = Seg (len p) by FINSEQ_1:def 3;
dom q = Seg (len p) by A3, FINSEQ_1:def 3;
then A5: dom (p + q) = dom p by A4, POLYNOM1:1;
then A6: len (p + q) = len p by A4, FINSEQ_1:def 3;
then A7: Indices (ACirc p) = Indices (ACirc (p + q)) by MATRIX_0:26;
A8: Indices (ACirc p) = Indices (ACirc q) by A3, MATRIX_0:26;
A9: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def 3;
A10: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;
then A11: len (- p) = len p by CARD_1:def 7;
A12: Indices (ACirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
p + q is first-line-of-anti-circular by A1, A2, A3, Th60;
then A13: ACirc (p + q) is_anti-circular_about p + q by Def12;
A14: ACirc q is_anti-circular_about q by A2, Def12;
A15: q is Element of (len q) -tuples_on the carrier of K by FINSEQ_2:92;
then - q is Element of (len q) -tuples_on the carrier of K by FINSEQ_2:113;
then A16: len (- q) = len q by CARD_1:def 7;
A17: ACirc p is_anti-circular_about p by A1, Def12;
A18: Indices (ACirc q) = [:(Seg (len p)),(Seg (len p)):] by A3, MATRIX_0:24;
A19: 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 A20: [i,j] in Indices (ACirc p) ; :: thesis: (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j))
then A21: ((j - i) mod (len p)) + 1 in Seg (len p) by A12, Lm3;

now :: thesis: ( ( i <= j & (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) ) or ( i >= j & (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) ) )

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

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

then (ACirc (p + q)) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) by A13, A7, A20
.= the addF of K . ((p . (((j - i) mod (len (p + q))) + 1)),(q . (((j - i) mod (len (p + q))) + 1))) by A9, A6, A21, FUNCOP_1:22
.= the addF of K . (((ACirc p) * (i,j)),(q . (((j - i) mod (len q)) + 1))) by A3, A6, A17, A20, A22
.= ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) by A14, A8, A20, A22 ;
hence (ACirc (p + q)) * (i,j) = ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) ; :: thesis: verum

end;

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

A24: dom (- p) = Seg (len p) by A11, FINSEQ_1:def 3;
dom (- q) = Seg (len q) by A16, FINSEQ_1:def 3;
then ( dom p = Seg (len p) & dom ((- p) + (- q)) = dom (- p) ) by A3, A24, FINSEQ_1:def 3, POLYNOM1:1;
then A25: ((j - i) mod (len (p + q))) + 1 in dom ((- p) + (- q)) by A9, A5, A12, A20, A24, Lm3;
(ACirc (p + q)) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) by A13, A7, A20, A23
.= ((- p) + (- q)) . (((j - i) mod (len (p + q))) + 1) by A3, A10, A15, FVSUM_1:31
.= the addF of K . (((- p) . (((j - i) mod (len (p + q))) + 1)),((- q) . (((j - i) mod (len (p + q))) + 1))) by A25, FUNCOP_1:22
.= the addF of K . (((ACirc p) * (i,j)),((- q) . (((j - i) mod (len q)) + 1))) by A3, A6, A17, A20, A23
.= ((ACirc p) * (i,j)) + ((ACirc q) * (i,j)) by A14, A12, A18, A20, A23 ;
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;

A26: ( len (ACirc p) = len p & width (ACirc p) = len p ) by MATRIX_0:24;
( len (ACirc (p + q)) = len p & width (ACirc (p + q)) = len p ) by A6, MATRIX_0:24;
hence ACirc (p + q) = (ACirc p) + (ACirc q) by A26, A19, MATRIX_3:def 3; :: thesis: verum