let K be Field; :: thesis: for a, b being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
(a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p)
let a, b be Element of K; :: thesis: for p being FinSequence of K st p is first-line-of-circulant holds
(a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p)
let p be FinSequence of K; :: thesis: ( p is first-line-of-circulant implies (a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p) )
set n = len p;
assume A1: p is first-line-of-circulant ; :: thesis: (a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p)
then A2: ( a * (LCirc p) = LCirc (a * p) & b * (LCirc p) = LCirc (b * p) ) by Th42;
A3: ( a * p is first-line-of-circulant & b * p is first-line-of-circulant ) by A1, Th41;
A4: ( len (a * p) = len p & len (b * p) = len p ) by MATRIXR1:16;
A5: (a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a * p) + (b * p)) by A2, A3, A4, Th34;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:110;
hence (a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p) by A5, FVSUM_1:68; :: thesis: verum