let n be Element of NAT ; :: thesis: for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is anti-circular holds
a * M1 is anti-circular
let K be Field; :: thesis: for a being Element of K
for M1 being Matrix of n,K st M1 is anti-circular holds
a * M1 is anti-circular
let a be Element of K; :: thesis: for M1 being Matrix of n,K st M1 is anti-circular holds
a * M1 is anti-circular
let M1 be Matrix of n,K; :: thesis: ( M1 is anti-circular implies a * M1 is anti-circular )
A1: Indices (a * M1) = [:(Seg n),(Seg n):] by MATRIX_0:24;
assume M1 is anti-circular ; :: thesis: a * M1 is anti-circular
then consider p being FinSequence of K such that
A2: len p = width M1 and
A3: M1 is_anti-circular_about p ;
A4: width M1 = n by MATRIX_0:24;
then A5: dom p = Seg n by A2, FINSEQ_1:def 3;
A6: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def 3;
A7: for i, j being Nat st [i,j] in Indices (a * M1) & i <= j holds
(a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (a * M1) & i <= j implies (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) )
assume that
A8: [i,j] in Indices (a * M1) and
A9: i <= j ; :: thesis: (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
A10: ((j - i) mod n) + 1 in Seg n by A1, A8, Lm3;
then A11: ((j - i) mod (len p)) + 1 in dom (a * p) by A2, A4, A6, MATRIXR1:16;
A12: [i,j] in Indices M1 by A1, A8, MATRIX_0:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def 5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . (p . (((j - i) mod (len p)) + 1)) by A3, A9, A12
.= (a multfield) . (p /. (((j - i) mod (len p)) + 1)) by A2, A4, A5, A10, PARTFUN1:def 6
.= a * (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * p) /. (((j - i) mod (len p)) + 1) by A2, A4, A5, A10, POLYNOM1:def 1
.= (a * p) . (((j - i) mod (len p)) + 1) by A11, PARTFUN1:def 6 ;
hence (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; :: thesis: verum

end;

A13: width (a * M1) = n by MATRIX_0:24;
A14: len p = n by A2, MATRIX_0:24;
A15: len (a * p) = len p by MATRIXR1:16;
for i, j being Nat st [i,j] in Indices (a * M1) & i >= j holds
(a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1)

proof

len (a * (- p)) = len (- p) by MATRIXR1:16;
then A16: dom (a * (- p)) = Seg (len (- p)) by FINSEQ_1:def 3
.= dom (- p) by FINSEQ_1:def 3 ;
A17: a * p is Element of n -tuples_on the carrier of K by A15, A14, FINSEQ_2:92;
let i, j be Nat; :: thesis: ( [i,j] in Indices (a * M1) & i >= j implies (a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1) )
assume that
A18: [i,j] in Indices (a * M1) and
A19: i >= j ; :: thesis: (a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1)
A20: ((j - i) mod n) + 1 in Seg n by A1, A18, Lm3;
A21: p is Element of n -tuples_on the carrier of K by A14, FINSEQ_2:92;
then - p is Element of (len p) -tuples_on the carrier of K by A14, FINSEQ_2:113;
then len (- p) = len p by CARD_1:def 7;
then A22: dom (- p) = Seg n by A2, A4, FINSEQ_1:def 3;
A23: [i,j] in Indices M1 by A1, A18, MATRIX_0:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def 5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . ((- p) . (((j - i) mod (len p)) + 1)) by A3, A19, A23
.= (a multfield) . ((- p) /. (((j - i) mod (len p)) + 1)) by A2, A4, A20, A22, PARTFUN1:def 6
.= a * ((- p) /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * (- p)) /. (((j - i) mod (len p)) + 1) by A2, A4, A20, A22, POLYNOM1:def 1
.= (a * (- p)) . (((j - i) mod (len p)) + 1) by A2, A4, A20, A22, A16, PARTFUN1:def 6
.= (a * ((- (1_ K)) * p)) . (((j - i) mod (len p)) + 1) by A21, FVSUM_1:59
.= ((a * (- (1_ K))) * p) . (((j - i) mod (len p)) + 1) by A21, FVSUM_1:54
.= ((- (a * (1_ K))) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:8
.= ((- a) * p) . (((j - i) mod (len p)) + 1)
.= ((- ((1_ K) * a)) * p) . (((j - i) mod (len p)) + 1)
.= (((- (1_ K)) * a) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:9
.= ((- (1_ K)) * (a * p)) . (((j - i) mod (len p)) + 1) by A21, FVSUM_1:54
.= (- (a * p)) . (((j - i) mod (len p)) + 1) by A17, FVSUM_1:59 ;
hence (a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; :: thesis: verum

end;

then a * M1 is_anti-circular_about a * p by A13, A15, A14, A7;
then consider q being FinSequence of K such that
A24: ( len q = width (a * M1) & a * M1 is_anti-circular_about q ) ;
take q ; :: according to MATRIX16:def 10 :: thesis: ( len q = width (a * M1) & a * M1 is_anti-circular_about q )
thus ( len q = width (a * M1) & a * M1 is_anti-circular_about q ) by A24; :: thesis: verum