let K be Field; :: thesis: for a being Element of K

for p being FinSequence of K st p is first-symmetry-of-circulant holds

a * p is first-symmetry-of-circulant

let a be Element of K; :: thesis: for p being FinSequence of K st p is first-symmetry-of-circulant holds

a * p is first-symmetry-of-circulant

let p be FinSequence of K; :: thesis: ( p is first-symmetry-of-circulant implies a * p is first-symmetry-of-circulant )

set n = len p;

A1: len (a * p) = len p by MATRIXR1:16;

assume p is first-symmetry-of-circulant ; :: thesis: a * p is first-symmetry-of-circulant

then consider M1 being Matrix of len p,K such that

A2: M1 is_symmetry_circulant_about p ;

a * M1 is_symmetry_circulant_about a * p by A2, Th3;

then consider M2 being Matrix of len (a * p),K such that

A3: M2 is_symmetry_circulant_about a * p by A1;

take M2 ; :: according to MATRIX17:def 6 :: thesis: M2 is_symmetry_circulant_about a * p

thus M2 is_symmetry_circulant_about a * p by A3; :: thesis: verum

for p being FinSequence of K st p is first-symmetry-of-circulant holds

a * p is first-symmetry-of-circulant

let a be Element of K; :: thesis: for p being FinSequence of K st p is first-symmetry-of-circulant holds

a * p is first-symmetry-of-circulant

let p be FinSequence of K; :: thesis: ( p is first-symmetry-of-circulant implies a * p is first-symmetry-of-circulant )

set n = len p;

A1: len (a * p) = len p by MATRIXR1:16;

assume p is first-symmetry-of-circulant ; :: thesis: a * p is first-symmetry-of-circulant

then consider M1 being Matrix of len p,K such that

A2: M1 is_symmetry_circulant_about p ;

a * M1 is_symmetry_circulant_about a * p by A2, Th3;

then consider M2 being Matrix of len (a * p),K such that

A3: M2 is_symmetry_circulant_about a * p by A1;

take M2 ; :: according to MATRIX17:def 6 :: thesis: M2 is_symmetry_circulant_about a * p

thus M2 is_symmetry_circulant_about a * p by A3; :: thesis: verum