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

for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds

(a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))

let a, b be Element of K; :: thesis: for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds

(a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))

let p, q be FinSequence of K; :: thesis: ( p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q implies (a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q)) )

set n = len p;

assume that

A1: p is first-symmetry-of-circulant and

A2: q is first-symmetry-of-circulant and

A3: len p = len q ; :: thesis: (a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))

A4: ( a * p is first-symmetry-of-circulant & b * q is first-symmetry-of-circulant ) by A1, A2, Th12;

A5: len (b * q) = len p by A3, MATRIXR1:16;

(a * (SCirc p)) + (b * (SCirc q)) = (SCirc (a * p)) + (b * (SCirc q)) by A1, Th13

.= (SCirc (a * p)) + (SCirc (b * q)) by A2, Th13

.= SCirc ((a * p) + (b * q)) by A4, A5, Th11, MATRIXR1:16 ;

hence (a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q)) ; :: thesis: verum

for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds

(a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))

let a, b be Element of K; :: thesis: for p, q being FinSequence of K st p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q holds

(a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))

let p, q be FinSequence of K; :: thesis: ( p is first-symmetry-of-circulant & q is first-symmetry-of-circulant & len p = len q implies (a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q)) )

set n = len p;

assume that

A1: p is first-symmetry-of-circulant and

A2: q is first-symmetry-of-circulant and

A3: len p = len q ; :: thesis: (a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q))

A4: ( a * p is first-symmetry-of-circulant & b * q is first-symmetry-of-circulant ) by A1, A2, Th12;

A5: len (b * q) = len p by A3, MATRIXR1:16;

(a * (SCirc p)) + (b * (SCirc q)) = (SCirc (a * p)) + (b * (SCirc q)) by A1, Th13

.= (SCirc (a * p)) + (SCirc (b * q)) by A2, Th13

.= SCirc ((a * p) + (b * q)) by A4, A5, Th11, MATRIXR1:16 ;

hence (a * (SCirc p)) + (b * (SCirc q)) = SCirc ((a * p) + (b * q)) ; :: thesis: verum