theorem :: MATRIX16:19

for i, j, k, n, l being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * (i,j) = A * (k,l)