let K be Field; :: thesis: for a being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
a * p is first-line-of-anti-circular
let a be Element of K; :: thesis: for p being FinSequence of K st p is first-line-of-anti-circular holds
a * p is first-line-of-anti-circular
let p be FinSequence of K; :: thesis: ( p is first-line-of-anti-circular implies a * p is first-line-of-anti-circular )
set n = len p;
A1: dom p = Seg (len p) by FINSEQ_1:def 3;
assume p is first-line-of-anti-circular ; :: thesis: a * p is first-line-of-anti-circular
then consider M1 being Matrix of len p,K such that
A2: M1 is_anti-circular_about p ;
A3: Indices (a * M1) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
A4: len (a * p) = len p by MATRIXR1:16;
A5: 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 A6: dom (a * (- p)) = Seg (len (- p)) by FINSEQ_1:def 3
.= dom (- p) by FINSEQ_1:def 3 ;
A7: a * p is Element of (len p) -tuples_on the carrier of K by A4, 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
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 (len p)) + 1 in Seg (len p) by A3, A8, Lm3;
A11: 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 A12: dom (- p) = Seg (len p) by FINSEQ_1:def 3;
A13: [i,j] in Indices M1 by A3, 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 A2, A9, A13
.= (a multfield) . ((- p) /. (((j - i) mod (len p)) + 1)) by A10, A12, PARTFUN1:def 6
.= a * ((- p) /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * (- p)) /. (((j - i) mod (len p)) + 1) by A10, A12, POLYNOM1:def 1
.= (a * (- p)) . (((j - i) mod (len p)) + 1) by A10, A12, A6, PARTFUN1:def 6
.= (a * ((- (1_ K)) * p)) . (((j - i) mod (len p)) + 1) by A11, FVSUM_1:59
.= ((a * (- (1_ K))) * p) . (((j - i) mod (len p)) + 1) by A11, 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 A11, FVSUM_1:54
.= (- (a * p)) . (((j - i) mod (len p)) + 1) by A7, FVSUM_1:59 ;
hence (a * M1) * (i,j) = (- (a * p)) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; :: thesis: verum

end;

A14: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def 3;
A15: 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
A16: [i,j] in Indices (a * M1) and
A17: i <= j ; :: thesis: (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
A18: ((j - i) mod (len p)) + 1 in Seg (len p) by A3, A16, Lm3;
then A19: ((j - i) mod (len p)) + 1 in dom (a * p) by A14, MATRIXR1:16;
A20: [i,j] in Indices M1 by A3, A16, 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 A2, A17, A20
.= (a multfield) . (p /. (((j - i) mod (len p)) + 1)) by A1, A18, PARTFUN1:def 6
.= a * (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * p) /. (((j - i) mod (len p)) + 1) by A1, A18, POLYNOM1:def 1
.= (a * p) . (((j - i) mod (len p)) + 1) by A19, PARTFUN1:def 6 ;
hence (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; :: thesis: verum

end;

width (a * M1) = len p by MATRIX_0:24;
then a * M1 is_anti-circular_about a * p by A4, A15, A5;
then consider M2 being Matrix of len (a * p),K such that
A21: M2 is_anti-circular_about a * p by A4;
take M2 ; :: according to MATRIX16:def 11 :: thesis: M2 is_anti-circular_about a * p
thus M2 is_anti-circular_about a * p by A21; :: thesis: verum