let n be Element of NAT ; :: thesis: for D being non empty set
for t being FinSequence of D
for A being Matrix of n,D st A is_col_circulant_about t & n > 0 holds
t = Col (A,1)
let D be non empty set ; :: thesis: for t being FinSequence of D
for A being Matrix of n,D st A is_col_circulant_about t & n > 0 holds
t = Col (A,1)
let t be FinSequence of D; :: thesis: for A being Matrix of n,D st A is_col_circulant_about t & n > 0 holds
t = Col (A,1)
let A be Matrix of n,D; :: thesis: ( A is_col_circulant_about t & n > 0 implies t = Col (A,1) )
assume that
A1: A is_col_circulant_about t and
A2: n > 0 ; :: thesis: t = Col (A,1)
A3: len A = n by MATRIX_0:24;
then A4: len t = n by A1;
A5: dom t = Seg (len t) by FINSEQ_1:def 3;
len (Col (A,1)) = n by A3, MATRIX_0:def 8;
then A6: dom (Col (A,1)) = dom t by A5, A4, FINSEQ_1:def 3;
for k being Nat st k in dom t holds
t . k = (Col (A,1)) . k

proof

let k be Nat; :: thesis: ( k in dom t implies t . k = (Col (A,1)) . k )
assume A7: k in dom t ; :: thesis: t . k = (Col (A,1)) . k
then A8: ( 1 <= k & k <= n ) by A5, A4, FINSEQ_1:1;
n >= 0 + 1 by A2, INT_1:7;
then 1 in Seg n ;
then [k,1] in [:(Seg n),(Seg n):] by A5, A4, A7, ZFMISC_1:def 2;
then A9: [k,1] in Indices A by MATRIX_0:24;
len (Col (A,1)) = len A by MATRIX_0:def 8;
then dom (Col (A,1)) = Seg (len A) by FINSEQ_1:def 3;
then k in dom A by A6, A7, FINSEQ_1:def 3;
then (Col (A,1)) . k = A * (k,1) by MATRIX_0:def 8
.= t . (((k - 1) mod (len t)) + 1) by A1, A9
.= t . ((k - 1) + 1) by A4, A8, Lm1 ;
hence t . k = (Col (A,1)) . k ; :: thesis: verum

end;

hence t = Col (A,1) by A6, FINSEQ_1:13; :: thesis: verum