theorem :: MATRIX16:18

for n being Element of NAT
for D being non empty set
for t being FinSequence of D
for A being Matrix of n,D st A is_col_circulant_about t & n > 0 holds
t = Col (A,1)