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_0:24;
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_0:26;

now :: thesis: ( ( i <= j & (ACirc (a * p)) * (i,j) = a * ((ACirc p) * (i,j)) ) or ( i >= j & (ACirc (a * p)) * (i,j) = a * ((ACirc p) * (i,j)) ) )

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
.= (a * p) /. (((j - i) mod (len p)) + 1) by A1, A8, A11, PARTFUN1:def 6
.= a * (p /. (((j - i) mod (len p)) + 1)) by A8, A12, POLYNOM1:def 1
.= (a multfield) . (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a multfield) . (p . (((j - i) mod (len p)) + 1)) by A8, A12, PARTFUN1:def 6
.= (a multfield) . ((ACirc p) * (i,j)) by A3, A7, A10
.= a * ((ACirc p) * (i,j)) by FVSUM_1:49 ;
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:92;
A16: 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 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:49
.= (a multfield) . ((- p) . (((j - i) mod (len p)) + 1)) by A3, A7, A13
.= (a multfield) . ((- p) /. (((j - i) mod (len p)) + 1)) by A8, A17, PARTFUN1:def 6
.= a * ((- p) /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * (- p)) /. (((j - i) mod (len p)) + 1) by A8, A17, POLYNOM1:def 1
.= (a * (- p)) . (((j - i) mod (len p)) + 1) by A8, A17, A14, PARTFUN1:def 6
.= (a * ((- (1_ K)) * p)) . (((j - i) mod (len p)) + 1) by A16, FVSUM_1:59
.= ((a * (- (1_ K))) * p) . (((j - i) mod (len p)) + 1) by A16, 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 A16, FVSUM_1:54
.= (- (a * p)) . (((j - i) mod (len p)) + 1) by A15, FVSUM_1:59
.= (ACirc (a * p)) * (i,j) by A1, A4, A9, A13 ;
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_0:24;
( len (ACirc (a * p)) = len p & width (ACirc (a * p)) = len p ) by A1, MATRIX_0:24;
hence ACirc (a * p) = a * (ACirc p) by A18, A6, MATRIX_3:def 5; :: thesis: verum