let n be Element of NAT ; :: thesis: for D being non empty set
for A being Matrix of n,D st A is line_circulant & n > 0 holds
A @ is col_circulant
let D be non empty set ; :: thesis: for A being Matrix of n,D st A is line_circulant & n > 0 holds
A @ is col_circulant
let A be Matrix of n,D; :: thesis: ( A is line_circulant & n > 0 implies A @ is col_circulant )
assume that
A1: A is line_circulant and
A2: n > 0 ; :: thesis: A @ is col_circulant
consider p being FinSequence of D such that
A3: len p = width A and
A4: A is_line_circulant_about p by A1, Def2;
width A = n by MATRIX_1:24;
then A5: len (A @) = len p by A2, A3, MATRIX_2:10;
for i, j being Nat st [i,j] in Indices (A @) holds
(A @) * (i,j) = p . (((i - j) mod (len p)) + 1)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (A @) implies (A @) * (i,j) = p . (((i - j) mod (len p)) + 1) )
A6: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume [i,j] in Indices (A @) ; :: thesis: (A @) * (i,j) = p . (((i - j) mod (len p)) + 1)
then [i,j] in Indices A by MATRIX_1:26;
then ( i in Seg n & j in Seg n ) by A6, ZFMISC_1:87;
then A7: [j,i] in Indices A by A6, ZFMISC_1:87;
then (A @) * (i,j) = A * (j,i) by MATRIX_1:def 6;
hence (A @) * (i,j) = p . (((i - j) mod (len p)) + 1) by A4, A7, Def1; :: thesis: verum

end;

then A @ is_col_circulant_about p by A5, Def4;
then consider p being FinSequence of D such that
A8: ( len p = len (A @) & A @ is_col_circulant_about p ) by A5;
take p ; :: according to MATRIX16:def 5 :: thesis: ( len p = len (A @) & A @ is_col_circulant_about p )
thus ( len p = len (A @) & A @ is_col_circulant_about p ) by A8; :: thesis: verum