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_{1} being Matrix of n,K st b_{1} = a * M1 holds

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

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

b