for K being Field
for p, q being FinSequence of K st len p = len q & p is first-col-of-circulant & q is first-col-of-circulant holds
CCirc (p + q) = (CCirc p) + (CCirc q)