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;
A1: len (a * p) = len p by MATRIXR1:16;
assume A2: p is first-line-of-circulant ; :: thesis: LCirc (a * p) = a * (LCirc p)
then a * p is first-line-of-circulant by Th41;
then A3: LCirc (a * p) is_line_circulant_about a * p by Def7;
A4: Indices (LCirc p) = [:(Seg (len p)),(Seg (len p)):] by MATRIX_0:24;
A5: LCirc p is_line_circulant_about p by A2, Def7;
A6: 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)) )
A7: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def 3;
assume A8: [i,j] in Indices (LCirc p) ; :: thesis: (LCirc (a * p)) * (i,j) = a * ((LCirc p) * (i,j))
then A9: ((j - i) mod (len p)) + 1 in Seg (len p) by A4, Lm3;
A10: dom p = Seg (len p) by FINSEQ_1:def 3;
[i,j] in Indices (LCirc (a * p)) by A1, A8, MATRIX_0:26;
then (LCirc (a * p)) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) by A3
.= (a * p) /. (((j - i) mod (len p)) + 1) by A1, A9, A7, PARTFUN1:def 6
.= a * (p /. (((j - i) mod (len p)) + 1)) by A9, A10, 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 A9, A10, PARTFUN1:def 6
.= (a multfield) . ((LCirc p) * (i,j)) by A5, A8
.= a * ((LCirc p) * (i,j)) by FVSUM_1:49 ;
hence (LCirc (a * p)) * (i,j) = a * ((LCirc p) * (i,j)) ; :: thesis: verum

end;

A11: ( len (LCirc p) = len p & width (LCirc p) = len p ) by MATRIX_0:24;
( len (LCirc (a * p)) = len p & width (LCirc (a * p)) = len p ) by A1, MATRIX_0:24;
hence LCirc (a * p) = a * (LCirc p) by A11, A6, MATRIX_3:def 5; :: thesis: verum