theorem :: MATRIX16:48

for K being Field
for a, b being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
(a * (CCirc p)) + (b * (CCirc p)) = CCirc ((a + b) * p)