theorem :: MATRIX16:50

for K being Field
for a, b 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 holds
(a * (CCirc p)) + (b * (CCirc q)) = CCirc ((a * p) + (b * q))