let K be Field; :: thesis: for a being Element of K
for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q & len p > 0 holds
(a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q))
let a be Element of K; :: thesis: for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q & len p > 0 holds
(a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q))
let p, q be FinSequence of K; :: thesis: ( p is first-col-of-circulant & q is first-col-of-circulant & len p = len q & len p > 0 implies (a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q)) )
set n = len p;
assume A1: ( p is first-col-of-circulant & q is first-col-of-circulant & len p = len q & len p > 0 ) ; :: thesis: (a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q))
A3: ( a * p is first-col-of-circulant & a * q is first-col-of-circulant & p + q is first-col-of-circulant ) by A1, Th37, Th46;
A5: ( len (CCirc q) = len p & len (CCirc p) = len p & width (CCirc q) = len p & width (CCirc p) = len p ) by A1, MATRIX_1:25;
(a * (CCirc p)) + (a * (CCirc q)) = a * ((CCirc p) + (CCirc q)) by A1, A5, MATRIX_5:36
.= a * (CCirc (p + q)) by A1, Th38
.= CCirc (a * (p + q)) by A3, Th47 ;
hence (a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q)) ; :: thesis: verum