theorem :: MATRIX16:64

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