let n be Element of NAT ; :: thesis: for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is line_circulant holds
a * M1 is line_circulant
let K be Field; :: thesis: for a being Element of K
for M1 being Matrix of n,K st M1 is line_circulant holds
a * M1 is line_circulant
let a be Element of K; :: thesis: for M1 being Matrix of n,K st M1 is line_circulant holds
a * M1 is line_circulant
let M1 be Matrix of n,K; :: thesis: ( M1 is line_circulant implies a * M1 is line_circulant )
A1: Indices (a * M1) = [:(Seg n),(Seg n):] by MATRIX_0:24;
assume M1 is line_circulant ; :: thesis: a * M1 is line_circulant
then consider p being FinSequence of K such that
A2: len p = width M1 and
A3: M1 is_line_circulant_about p ;
A4: width M1 = n by MATRIX_0:24;
then A5: dom p = Seg n by A2, FINSEQ_1:def 3;
A6: dom (a * p) = Seg (len (a * p)) by FINSEQ_1:def 3;
A7: for i, j being Nat st [i,j] in Indices (a * M1) holds
(a * M1) * (i,j) = (a * p) . (((j - i) 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) . (((j - i) mod (len (a * p))) + 1) )
assume A8: [i,j] in Indices (a * M1) ; :: thesis: (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1)
then A9: ((j - i) mod n) + 1 in Seg n by A1, Lm3;
then A10: ((j - i) mod (len p)) + 1 in dom (a * p) by A2, A4, A6, MATRIXR1:16;
A11: [i,j] in Indices M1 by A1, A8, MATRIX_0:24;
then (a * M1) * (i,j) = a * (M1 * (i,j)) by MATRIX_3:def 5
.= (a multfield) . (M1 * (i,j)) by FVSUM_1:49
.= (a multfield) . (p . (((j - i) mod (len p)) + 1)) by A3, A11
.= (a multfield) . (p /. (((j - i) mod (len p)) + 1)) by A2, A4, A5, A9, PARTFUN1:def 6
.= a * (p /. (((j - i) mod (len p)) + 1)) by FVSUM_1:49
.= (a * p) /. (((j - i) mod (len p)) + 1) by A2, A4, A5, A9, POLYNOM1:def 1
.= (a * p) . (((j - i) mod (len p)) + 1) by A10, PARTFUN1:def 6 ;
hence (a * M1) * (i,j) = (a * p) . (((j - i) mod (len (a * p))) + 1) by MATRIXR1:16; :: thesis: verum

end;

A12: ( width (a * M1) = n & len (a * p) = len p ) by MATRIXR1:16, MATRIX_0:24;
len p = n by A2, MATRIX_0:24;
then a * M1 is_line_circulant_about a * p by A12, A7;
then consider q being FinSequence of K such that
A13: ( len q = width (a * M1) & a * M1 is_line_circulant_about q ) ;
take q ; :: according to MATRIX16:def 2 :: thesis: ( len q = width (a * M1) & a * M1 is_line_circulant_about q )
thus ( len q = width (a * M1) & a * M1 is_line_circulant_about q ) by A13; :: thesis: verum