let n be Element of NAT ; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 + M2 is anti-circular
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 + M2 is anti-circular
let M1, M2 be Matrix of n,K; :: thesis: ( M1 is anti-circular & M2 is anti-circular implies M1 + M2 is anti-circular )
assume that
A1: M1 is anti-circular and
A2: M2 is anti-circular ; :: thesis: M1 + M2 is anti-circular
consider p being FinSequence of K such that
A3: len p = width M1 and
A4: M1 is_anti-circular_about p by A1;
A5: width M1 = n by MATRIX_0:24;
then A6: dom p = Seg n by A3, FINSEQ_1:def 3;
consider q being FinSequence of K such that
A7: len q = width M2 and
A8: M2 is_anti-circular_about q by A2;
A9: dom (p + q) = Seg (len (p + q)) by FINSEQ_1:def 3;
A10: width M2 = n by MATRIX_0:24;
then dom q = Seg n by A7, FINSEQ_1:def 3;
then A11: dom (p + q) = dom p by A6, POLYNOM1:1;
then A12: len (p + q) = n by A6, FINSEQ_1:def 3;
A13: 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 len (- p) = len p by CARD_1:def 7;
then A14: dom (- p) = Seg n by A3, A5, FINSEQ_1:def 3;
A15: Indices M2 = [:(Seg n),(Seg n):] by MATRIX_0:24;
A16: Indices (M1 + M2) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A17: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_0:24;
A18: 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 len (- q) = len q by CARD_1:def 7;
then A19: dom (- q) = Seg n by A7, A10, FINSEQ_1:def 3;
A20: 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
A21: [i,j] in Indices (M1 + M2) and
A22: i >= j ; :: thesis: (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1)
dom ((- p) + (- q)) = dom (- p) by A14, A19, POLYNOM1:1;
then A23: ((j - i) mod (len (p + q))) + 1 in dom ((- p) + (- q)) by A16, A6, A9, A14, A11, A21, Lm3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A17, A16, A21, MATRIX_3:def 3
.= the addF of K . ((M1 * (i,j)),((- q) . (((j - i) mod (len q)) + 1))) by A8, A15, A16, A21, A22
.= the addF of K . (((- p) . (((j - i) mod (len (p + q))) + 1)),((- q) . (((j - i) mod (len (p + q))) + 1))) by A4, A7, A17, A5, A10, A16, A12, A21, A22
.= ((- p) + (- q)) . (((j - i) mod (len (p + q))) + 1) by A23, FUNCOP_1:22
.= (- (p + q)) . (((j - i) mod (len (p + q))) + 1) by A3, A7, A13, A18, A5, A10, FVSUM_1:31 ;
hence (M1 + M2) * (i,j) = (- (p + q)) . (((j - i) mod (len (p + q))) + 1) ; :: thesis: verum

end;

A24: width (M1 + M2) = n by MATRIX_0:24;
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
A25: [i,j] in Indices (M1 + M2) and
A26: i <= j ; :: thesis: (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1)
A27: ((j - i) mod (len (p + q))) + 1 in dom (p + q) by A16, A6, A9, A11, A25, Lm3;
(M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by A17, A16, A25, MATRIX_3:def 3
.= the addF of K . ((M1 * (i,j)),(q . (((j - i) mod (len q)) + 1))) by A8, A15, A16, A25, A26
.= the addF of K . ((p . (((j - i) mod (len (p + q))) + 1)),(q . (((j - i) mod (len (p + q))) + 1))) by A4, A7, A17, A5, A10, A16, A12, A25, A26
.= (p + q) . (((j - i) mod (len (p + q))) + 1) by A27, FUNCOP_1:22 ;
hence (M1 + M2) * (i,j) = (p + q) . (((j - i) mod (len (p + q))) + 1) ; :: thesis: verum

end;

then M1 + M2 is_anti-circular_about p + q by A24, A12, A20;
then consider r being FinSequence of K such that
A28: ( len r = width (M1 + M2) & M1 + M2 is_anti-circular_about r ) ;
take r ; :: according to MATRIX16:def 10 :: thesis: ( len r = width (M1 + M2) & M1 + M2 is_anti-circular_about r )
thus ( len r = width (M1 + M2) & M1 + M2 is_anti-circular_about r ) by A28; :: thesis: verum