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
ACirc (a * p) = a * (ACirc p)
let a be Element of K; :: thesis: for p being FinSequence of K st p is first-line-of-anti-circular holds
ACirc (a * p) = a * (ACirc p)
let p be FinSequence of K; :: thesis: ( p is first-line-of-anti-circular implies ACirc (a * p) = a * (ACirc p) )
set n = len p;
A1: len (a * p) = len p by MATRIXR1:16;
assume A2: p is first-line-of-anti-circular ; :: thesis: ACirc (a * p) = a * (ACirc p)
then A3: ACirc p is_anti-circular_about p by Def12;
a * p is first-line-of-anti-circular by A2, Th62;
then A4: ACirc (a * p) is_anti-circular_about a * p by Def12;
A5: Indices (ACirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_1:25;
A6: for i, j being Nat st [i,j] in Indices (ACirc p) holds
(ACirc (a * p)) * i,j = a * ((ACirc p) * i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (ACirc p) implies (ACirc (a * p)) * i,j = a * ((ACirc p) * i,j) )
assume A7: [i,j] in Indices (ACirc p) ; :: thesis: (ACirc (a * p)) * i,j = a * ((ACirc p) * i,j)
then A8: ((j - i) mod (len p)) + 1 in Seg (len p) by A5, Lm3;
A9: [i,j] in Indices (ACirc (a * p)) by A1, A7, MATRIX_1:27;

now

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

case A10: i <= j ; :: thesis: (ACirc (a * p)) * i,j = a * ((ACirc p) * i,j)

A11: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def 3;
A12: dom p = Seg (len p) by FINSEQ_1:def 3;
(ACirc (a * p)) * i,j = (a * p) . (((j - i) mod (len (a * p))) + 1) by A4, A9, A10, Def9
.= (a * p) /. (((j - i) mod (len p)) + 1) by A1, A8, A11, PARTFUN1:def 8
.= a * (p /. (((j - i) mod (len p)) + 1)) by A8, A12, POLYNOM1:def 2
.= (a multfield ) . (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:61
.= (a multfield ) . (p . (((j - i) mod (len p)) + 1)) by A8, A12, PARTFUN1:def 8
.= (a multfield ) . ((ACirc p) * i,j) by A3, A7, A10, Def9
.= a * ((ACirc p) * i,j) by FVSUM_1:61 ;
hence (ACirc (a * p)) * i,j = a * ((ACirc p) * i,j) ; :: thesis: verum

end;

case A13: i >= j ; :: thesis: (ACirc (a * p)) * i,j = a * ((ACirc p) * i,j)

len (a * (- p)) = len (- p) by MATRIXR1:16;
then A14: dom (a * (- p)) = Seg (len (- p)) by FINSEQ_1:def 3
.= dom (- p) by FINSEQ_1:def 3 ;
A15: a * p is Element of (len p) -tuples_on the carrier of K by A1, FINSEQ_2:110;
A16: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:110;
then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:133;
then len (- p) = len p by FINSEQ_1:def 18;
then A17: dom (- p) = Seg (len p) by FINSEQ_1:def 3;
a * ((ACirc p) * i,j) = (a multfield ) . ((ACirc p) * i,j) by FVSUM_1:61
.= (a multfield ) . ((- p) . (((j - i) mod (len p)) + 1)) by A3, A7, A13, Def9
.= (a multfield ) . ((- p) /. (((j - i) mod (len p)) + 1)) by A8, A17, PARTFUN1:def 8
.= a * ((- p) /. (((j - i) mod (len p)) + 1)) by FVSUM_1:61
.= (a * (- p)) /. (((j - i) mod (len p)) + 1) by A8, A17, POLYNOM1:def 2
.= (a * (- p)) . (((j - i) mod (len p)) + 1) by A8, A17, A14, PARTFUN1:def 8
.= (a * ((- (1_ K)) * p)) . (((j - i) mod (len p)) + 1) by A16, FVSUM_1:72
.= ((a * (- (1_ K))) * p) . (((j - i) mod (len p)) + 1) by A16, FVSUM_1:67
.= ((- (a * (1_ K))) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:40
.= ((- a) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:def 16
.= ((- ((1_ K) * a)) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:def 16
.= (((- (1_ K)) * a) * p) . (((j - i) mod (len p)) + 1) by VECTSP_1:41
.= ((- (1_ K)) * (a * p)) . (((j - i) mod (len p)) + 1) by A16, FVSUM_1:67
.= (- (a * p)) . (((j - i) mod (len p)) + 1) by A15, FVSUM_1:72
.= (ACirc (a * p)) * i,j by A1, A4, A9, A13, Def9 ;
hence (ACirc (a * p)) * i,j = a * ((ACirc p) * i,j) ; :: thesis: verum

end;

end;

end;

hence (ACirc (a * p)) * i,j = a * ((ACirc p) * i,j) ; :: thesis: verum

end;

A18: ( len (ACirc p) = len p & width (ACirc p) = len p ) by MATRIX_1:25;
( len (ACirc (a * p)) = len p & width (ACirc (a * p)) = len p ) by A1, MATRIX_1:25;
hence ACirc (a * p) = a * (ACirc p) by A18, A6, MATRIX_3:def 5; :: thesis: verum