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 A1: ( A is line_circulant & n > 0 ) ; :: thesis: A @ is col_circulant
then consider p being FinSequence of D such that
A2: ( len p = width A & A is_line_circulant_about p ) by Def2;
( len A = n & width A = n ) by MATRIX_1:25;
then A6: len (A @ ) = len p by A2, A1, MATRIX_2:12;
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) )
assume [i,j] in Indices (A @ ) ; :: thesis: (A @ ) * i,j = p . (((i - j) mod (len p)) + 1)
then B2: [i,j] in Indices A by MATRIX_1:27;
B3: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:25;
then ( i in Seg n & j in Seg n ) by B2, ZFMISC_1:106;
then B5: [j,i] in Indices A by B3, ZFMISC_1:106;
then (A @ ) * i,j = A * j,i by MATRIX_1:def 7;
hence (A @ ) * i,j = p . (((i - j) mod (len p)) + 1) by A2, Def1, B5; :: thesis: verum

end;

then A10: A @ is_col_circulant_about p by A6, Def4;
consider p being FinSequence of D such that
A11: ( len p = len (A @ ) & A @ is_col_circulant_about p ) by A6, A10;
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 A11; :: thesis: verum