set p = n |-> a;

(n,n) --> a is_symmetry_circulant_about n |-> a by Th2;

hence for b_{1} being Matrix of n,K st b_{1} = (n,n) --> a holds

b_{1} is symmetry_circulant
; :: thesis: verum

(n,n) --> a is_symmetry_circulant_about n |-> a by Th2;

hence for b

b