:: deftheorem Def7 defines SCirc MATRIX17:def 7 :
for K being non empty set
for p being FinSequence of K st p is first-symmetry-of-circulant holds
for b₃ being Matrix of len p,K holds
( b₃ = SCirc p iff b₃ is_symmetry_circulant_about p );