consider p being FinSequence of K such that
len p = width M1 and
A1: M1 is_symmetry_circulant_about p by Def5;
a * M1 is_symmetry_circulant_about a * p by A1, Th3;
then ex q being FinSequence of K st
( len q = width (a * M1) & a * M1 is_symmetry_circulant_about q ) ;
hence for b₁ being Matrix of n,K st b₁ = a * M1 holds
b₁ is symmetry_circulant ; :: thesis: verum