theorem :: MATRIX16:49

for K being Field
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))