theorem :: MATRIX17:14

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