let K be Field; :: thesis: for p being FinSequence of K st p is first-symmetry-of-circulant holds

- p is first-symmetry-of-circulant

let p be FinSequence of K; :: thesis: ( p is first-symmetry-of-circulant implies - p is first-symmetry-of-circulant )

set n = len p;

assume p is first-symmetry-of-circulant ; :: thesis: - p is first-symmetry-of-circulant

then consider M1 being Matrix of len p,K such that

A1: M1 is_symmetry_circulant_about p ;

p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;

then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;

then A2: len (- p) = len p by CARD_1:def 7;

- M1 is_symmetry_circulant_about - p by A1, Th4;

then consider M2 being Matrix of len (- p),K such that

A3: M2 is_symmetry_circulant_about - p by A2;

take M2 ; :: according to MATRIX17:def 6 :: thesis: M2 is_symmetry_circulant_about - p

thus M2 is_symmetry_circulant_about - p by A3; :: thesis: verum

- p is first-symmetry-of-circulant

let p be FinSequence of K; :: thesis: ( p is first-symmetry-of-circulant implies - p is first-symmetry-of-circulant )

set n = len p;

assume p is first-symmetry-of-circulant ; :: thesis: - p is first-symmetry-of-circulant

then consider M1 being Matrix of len p,K such that

A1: M1 is_symmetry_circulant_about p ;

p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;

then - p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:113;

then A2: len (- p) = len p by CARD_1:def 7;

- M1 is_symmetry_circulant_about - p by A1, Th4;

then consider M2 being Matrix of len (- p),K such that

A3: M2 is_symmetry_circulant_about - p by A2;

take M2 ; :: according to MATRIX17:def 6 :: thesis: M2 is_symmetry_circulant_about - p

thus M2 is_symmetry_circulant_about - p by A3; :: thesis: verum