let K be Field; :: thesis: for a being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
a * p is first-col-of-circulant
let a be Element of K; :: thesis: for p being FinSequence of K st p is first-col-of-circulant holds
a * p is first-col-of-circulant
let p be FinSequence of K; :: thesis: ( p is first-col-of-circulant implies a * p is first-col-of-circulant )
set n = len p;
assume A1: p is first-col-of-circulant ; :: thesis: a * p is first-col-of-circulant
consider M1 being Matrix of len p,K such that
A2: M1 is_col_circulant_about p by A1, Def6;
A5: ( Indices (a * M1) = [:(Seg (len p)),(Seg (len p)):] & len (a * M1) = len p & width (a * M1) = len p ) by MATRIX_1:25;
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;
for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * i,j = (a * p) . (((i - j) mod (len (a * p))) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (a * M1) implies (a * M1) * i,j = (a * p) . (((i - j) mod (len (a * p))) + 1) )
assume B1: [i,j] in Indices (a * M1) ; :: thesis: (a * M1) * i,j = (a * p) . (((i - j) mod (len (a * p))) + 1)
then B2: [i,j] in Indices M1 by MATRIX_1:25, A5;
B3: ((i - j) mod (len p)) + 1 in Seg (len p) by B1, A5, Lm2;
then B23: ( ((i - j) mod (len p)) + 1 in dom (a * p) & ((i - j) mod (len p)) + 1 in dom p ) by A7, MATRIXR1:16;
(a * M1) * i,j = a * (M1 * i,j) by B2, MATRIX_3:def 5
.= (a multfield ) . (M1 * i,j) by FVSUM_1:61
.= (a multfield ) . (p . (((i - j) mod (len p)) + 1)) by B2, A2, Def4
.= (a multfield ) . (p /. (((i - j) mod (len p)) + 1)) by B3, A7, PARTFUN1:def 8
.= a * (p /. (((i - j) mod (len p)) + 1)) by FVSUM_1:61
.= (a * p) /. (((i - j) mod (len p)) + 1) by B3, A7, POLYNOM1:def 2
.= (a * p) . (((i - j) mod (len p)) + 1) by B23, PARTFUN1:def 8 ;
hence (a * M1) * i,j = (a * p) . (((i - j) mod (len (a * p))) + 1) by MATRIXR1:16; :: thesis: verum

end;

then A9: a * M1 is_col_circulant_about a * p by A5, A6, Def4;
set M2 = a * M1;
consider M2 being Matrix of len (a * p),K such that
A11: M2 is_col_circulant_about a * p by A6, A9;
take M2 ; :: according to MATRIX16:def 6 :: thesis: M2 is_col_circulant_about a * p
thus M2 is_col_circulant_about a * p by A11; :: thesis: verum