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
p + q is first-line-of-anti-circular
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 p + q is first-line-of-anti-circular )
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: p + q is first-line-of-anti-circular
consider M2 being Matrix of len p,K such that
A4: M2 is_anti-circular_about q by A2, A3;
A5: width M2 = len p by MATRIX_0:24;
A6: dom p = Seg (len p) by FINSEQ_1:def 3;
len q = width M2 by A4;
then dom q = Seg (len p) by A5, FINSEQ_1:def 3;
then A7: dom (p + q) = dom p by A6, POLYNOM1:1;
then A8: len (p + q) = len p by A6, FINSEQ_1:def 3;
consider M1 being Matrix of len p,K such that
A9: M1 is_anti-circular_about p by A1;
A10: Indices M1 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
set M3 = M1 + M2;
A11: 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 A12: len (- q) = len q by CARD_1:def 7;
A13: Indices M2 = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
A14: Indices (M1 + M2) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
A15: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def 3;
A16: for i, j being Nat st [i,j] in Indices (M1 + M2) & i <= j holds
(M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (M1 + M2) & i <= j implies (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) )
assume that
A17: [i,j] in Indices (M1 + M2) and
A18: i <= j ; :: thesis: (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
A19: ((j - i) mod (len (p + q))) + 1 in dom (p + q) by A14, A6, A15, A7, A17, Lm3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A10, A14, A17, MATRIX_3:def 3
.= the addF of K . ((M1 * (i,j)),(q . (((j - i) mod (len q)) + 1))) by A4, A13, A14, A17, A18
.= the addF of K . ((p . (((j - i) mod (len (p + q))) + 1)),(q . (((j - i) mod (len (p + q))) + 1))) by A3, A9, A10, A14, A8, A17, A18
.= (p + q) . (((j - i) mod (len (p + q))) + 1) by A19, FUNCOP_1:22 ;
hence (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) ; :: thesis: verum

end;

A20: 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 A21: len (- p) = len p by CARD_1:def 7;
then A22: dom (- p) = Seg (len p) by FINSEQ_1:def 3;
A23: for i, j being Nat st [i,j] in Indices (M1 + M2) & i >= j holds
(M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (M1 + M2) & i >= j implies (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) )
assume that
A24: [i,j] in Indices (M1 + M2) and
A25: i >= j ; :: thesis: (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
( dom (- p) = Seg (len p) & dom (- q) = Seg (len q) ) by A21, A12, FINSEQ_1:def 3;
then dom ((- p) + (- q)) = dom (- p) by A3, POLYNOM1:1;
then A26: ((j - i) mod (len (p + q))) + 1 in dom ((- p) + (- q)) by A14, A6, A15, A22, A7, A24, Lm3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A10, A14, A24, MATRIX_3:def 3
.= the addF of K . ((M1 * (i,j)),((- q) . (((j - i) mod (len q)) + 1))) by A4, A13, A14, A24, A25
.= the addF of K . (((- p) . (((j - i) mod (len p)) + 1)),((- q) . (((j - i) mod (len q)) + 1))) by A9, A10, A14, A24, A25
.= ((- p) + (- q)) . (((j - i) mod (len (p + q))) + 1) by A3, A8, A26, FUNCOP_1:22
.= (- (p + q)) . (((j - i) mod (len (p + q))) + 1) by A3, A20, A11, FVSUM_1:31 ;
hence (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) ; :: thesis: verum

end;

width (M1 + M2) = len p by MATRIX_0:24;
then len (p + q) = width (M1 + M2) by A6, A7, FINSEQ_1:def 3;
then ( len (M1 + M2) = len p & M1 + M2 is_anti-circular_about p + q ) by A16, A23, MATRIX_0:24;
then consider M3 being Matrix of len (p + q),K such that
len (p + q) = len M3 and
A27: M3 is_anti-circular_about p + q by A8;
take M3 ; :: according to MATRIX16:def 11 :: thesis: M3 is_anti-circular_about p + q
thus M3 is_anti-circular_about p + q by A27; :: thesis: verum