take (1,1) --> (0. K) ; :: thesis: ( (1,1) --> (0. K) is line_circulant & (1,1) --> (0. K) is col_circulant )
thus ( (1,1) --> (0. K) is line_circulant & (1,1) --> (0. K) is col_circulant ) ; :: thesis: verum