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

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (A @) implies (A @) * (i,j) = p . (((j - i) mod (len p)) + 1) )
A6: Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24;
assume [i,j] in Indices (A @) ; :: thesis: (A @) * (i,j) = p . (((j - i) mod (len p)) + 1)
then [i,j] in Indices A by MATRIX_0: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_0:def 6;
hence (A @) * (i,j) = p . (((j - i) mod (len p)) + 1) by A4, A7; :: thesis: verum

end;

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