theorem :: MATRIX16:65

for K being Field
for a being Element of K
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
(a * (ACirc p)) + (a * (ACirc q)) = ACirc (a * (p + q))