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;
assume A1: p is first-line-of-anti-circular ; :: thesis: ACirc (a * p) = a * (ACirc p)
then A2: a * p is first-line-of-anti-circular by Th62;
A6: ( len (a * p) = len p & len p = len p ) by MATRIXR1:16;
A7: ( dom p = Seg (len p) & dom (a * p) = Seg (len (a * p)) & dom p = Seg (len p) ) by FINSEQ_1:def 3;
A10: ACirc p is_anti-circular_about p by A1, Def13;
A12: ACirc (a * p) is_anti-circular_about a * p by A2, Def13;
A13: ( len (ACirc (a * p)) = len p & len (ACirc p) = len p & width (ACirc (a * p)) = len p & width (ACirc p) = len p ) by A6, MATRIX_1:25;
A15: ( Indices (ACirc p) = Indices (ACirc (a * p)) & Indices (ACirc p) = [:(Seg (len p)),(Seg (len p)):] ) by A6, MATRIX_1:25, MATRIX_1:27;
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 B1: [i,j] in Indices (ACirc p) ; :: thesis: (ACirc (a * p)) * i,j = a * ((ACirc p) * i,j)
then B2: [i,j] in Indices (ACirc (a * p)) by A6, MATRIX_1:27;
B3: ((j - i) mod (len p)) + 1 in Seg (len p) by B1, A15, Lm2;

now

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

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

B4: ( dom (a * p) = Seg (len (a * p)) & 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 C1, B2, A12, Def10
.= (a * p) /. (((j - i) mod (len p)) + 1) by A6, B3, B4, PARTFUN1:def 8
.= a * (p /. (((j - i) mod (len p)) + 1)) by B3, B4, 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 B3, B4, PARTFUN1:def 8
.= (a multfield ) . ((ACirc p) * i,j) by C1, B1, A10, Def10
.= a * ((ACirc p) * i,j) by FVSUM_1:61 ;
hence (ACirc (a * p)) * i,j = a * ((ACirc p) * i,j) ; :: thesis: verum

end;

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

D: ( p is Element of (len p) -tuples_on the carrier of K & a * p is Element of (len p) -tuples_on the carrier of K ) by A6, 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 B7: ( dom (- p) = Seg (len p) & dom (- p) = dom p ) by A7, FINSEQ_1:def 3;
len (a * (- p)) = len (- p) by MATRIXR1:16;
then B8: dom (a * (- p)) = Seg (len (- p)) by FINSEQ_1:def 3
.= dom (- 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 C2, B1, A10, Def10
.= (a multfield ) . ((- p) /. (((j - i) mod (len p)) + 1)) by B3, B7, PARTFUN1:def 8
.= a * ((- p) /. (((j - i) mod (len p)) + 1)) by FVSUM_1:61
.= (a * (- p)) /. (((j - i) mod (len p)) + 1) by B3, B7, POLYNOM1:def 2
.= (a * (- p)) . (((j - i) mod (len p)) + 1) by B3, B7, B8, PARTFUN1:def 8
.= (a * ((- (1_ K)) * p)) . (((j - i) mod (len p)) + 1) by D, FVSUM_1:72
.= ((a * (- (1_ K))) * p) . (((j - i) mod (len p)) + 1) by D, 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 D, FVSUM_1:67
.= (- (a * p)) . (((j - i) mod (len p)) + 1) by D, FVSUM_1:72
.= (ACirc (a * p)) * i,j by C2, B2, A12, Def10, A6 ;
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;

hence ACirc (a * p) = a * (ACirc p) by A13, MATRIX_3:def 5; :: thesis: verum