let n be Nat; :: thesis: for D being non empty set
for A being Matrix of n,D st A is symmetry_circulant & n > 0 holds
A @ is symmetry_circulant
let D be non empty set ; :: thesis: for A being Matrix of n,D st A is symmetry_circulant & n > 0 holds
A @ is symmetry_circulant
let A be Matrix of n,D; :: thesis: ( A is symmetry_circulant & n > 0 implies A @ is symmetry_circulant )
assume that
A1: A is symmetry_circulant and
A2: n > 0 ; :: thesis: A @ is symmetry_circulant
consider p being FinSequence of D such that
A3: len p = width A and
A4: A is_symmetry_circulant_about p by A1;
( width A = n & len A = n ) by MATRIX_0:24;
then width (A @) = len p by A2, A3, MATRIX_0:54;
then consider p being FinSequence of D such that
A5: ( len p = width (A @) & A @ is_symmetry_circulant_about p ) by A2, A4, Th6;
take p ; :: according to MATRIX17:def 5 :: thesis: ( len p = width (A @) & A @ is_symmetry_circulant_about p )
thus ( len p = width (A @) & A @ is_symmetry_circulant_about p ) by A5; :: thesis: verum