set p = n |-> a;
A1: ( width ((n,n) --> a) = n & len (n |-> a) = n ) by CARD_1:def 7, MATRIX_1:24;
(n,n) --> a is_symmetry_circulant_about n |-> a by T1;
hence for b₁ being Matrix of n,K st b₁ = (n,n) --> a holds
b₁ is symmetry_circulant by A1, Def5; :: thesis: verum