for n being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is line_circulant & n > 0 holds
A @ is col_circulant