let K be Field; :: thesis: for a being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
LCirc (a * p) = a * (LCirc p)
let a be Element of K; :: thesis: for p being FinSequence of K st p is first-line-of-circulant holds
LCirc (a * p) = a * (LCirc p)
let p be FinSequence of K; :: thesis: ( p is first-line-of-circulant implies LCirc (a * p) = a * (LCirc p) )
set n = len p;
assume A1: p is first-line-of-circulant ; :: thesis: LCirc (a * p) = a * (LCirc p)
then A4: a * p is first-line-of-circulant by Th41;
A6: len (a * p) = len p by MATRIXR1:16;
A10: LCirc p is_line_circulant_about p by A1, Def7;
A12: LCirc (a * p) is_line_circulant_about a * p by A4, Def7;
A13: ( len (LCirc (a * p)) = len p & len (LCirc p) = len p & width (LCirc (a * p)) = len p & width (LCirc p) = len p ) by A6, MATRIX_1:25;
A15: ( Indices (LCirc p) = Indices (LCirc (a * p)) & Indices (LCirc 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 (LCirc p) holds
(LCirc (a * p)) * i,j = a * ((LCirc p) * i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (LCirc p) implies (LCirc (a * p)) * i,j = a * ((LCirc p) * i,j) )
assume B1: [i,j] in Indices (LCirc p) ; :: thesis: (LCirc (a * p)) * i,j = a * ((LCirc p) * i,j)
then B2: [i,j] in Indices (LCirc (a * p)) by A6, MATRIX_1:27;
B3: ((j - i) mod (len p)) + 1 in Seg (len p) by B1, A15, Lm2;
B4: ( dom (a * p) = Seg (len (a * p)) & dom p = Seg (len p) ) by FINSEQ_1:def 3;
(LCirc (a * p)) * i,j = (a * p) . (((j - i) mod (len (a * p))) + 1) by B2, A12, Def1
.= (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 ) . ((LCirc p) * i,j) by B1, A10, Def1
.= a * ((LCirc p) * i,j) by FVSUM_1:61 ;
hence (LCirc (a * p)) * i,j = a * ((LCirc p) * i,j) ; :: thesis: verum

end;

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