set p = n |-> a;
(n,n) --> a is_symmetry_circulant_about n |-> a by Th2;
hence for b₁ being Matrix of n,K st b₁ = (n,n) --> a holds
b₁ is symmetry_circulant ; :: thesis: verum