take (n,n) --> (0. K) ; :: thesis: (n,n) --> (0. K) is symmetry_circulant
thus (n,n) --> (0. K) is symmetry_circulant ; :: thesis: verum