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

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

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

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

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

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

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

A2: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;

assume A3: p is first-symmetry-of-circulant ; :: thesis: (a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p)

then A4: ( a * p is first-symmetry-of-circulant & b * p is first-symmetry-of-circulant ) by Th12;

( a * (SCirc p) = SCirc (a * p) & b * (SCirc p) = SCirc (b * p) ) by A3, Th13;

then (a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a * p) + (b * p)) by A4, A1, Th11, MATRIXR1:16;

hence (a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p) by A2, FVSUM_1:55; :: thesis: verum

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

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

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

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

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

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

A2: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;

assume A3: p is first-symmetry-of-circulant ; :: thesis: (a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p)

then A4: ( a * p is first-symmetry-of-circulant & b * p is first-symmetry-of-circulant ) by Th12;

( a * (SCirc p) = SCirc (a * p) & b * (SCirc p) = SCirc (b * p) ) by A3, Th13;

then (a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a * p) + (b * p)) by A4, A1, Th11, MATRIXR1:16;

hence (a * (SCirc p)) + (b * (SCirc p)) = SCirc ((a + b) * p) by A2, FVSUM_1:55; :: thesis: verum