theorem :: MATRIX17:15

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