consider p being FinSequence of K such that
A2: len p = width M1 and
A3: M1 is_symmetry_circulant_about p by Def5;
A4: ( width (a * M1) = n & len (a * p) = len p ) by MATRIXR1:16, MATRIX_1:24;
a * M1 is_symmetry_circulant_about a * p by A3, T2;
then ex q being FinSequence of K st
( len q = width (a * M1) & a * M1 is_symmetry_circulant_about q ) by A2, A4, MATRIX_1:24;
hence for b₁ being Matrix of n,K st b₁ = a * M1 holds
b₁ is symmetry_circulant by Def5; :: thesis: verum