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_line_circulant_about t & n > 0 holds
t = Line (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_line_circulant_about t & n > 0 holds
t = Line (A,1)
let t be FinSequence of D; :: thesis: for A being Matrix of n,D st A is_line_circulant_about t & n > 0 holds
t = Line (A,1)
let A be Matrix of n,D; :: thesis: ( A is_line_circulant_about t & n > 0 implies t = Line (A,1) )
assume that
A1: A is_line_circulant_about t and
A2: n > 0 ; :: thesis: t = Line (A,1)
A3: width A = n by MATRIX_1:24;
then A4: ( dom t = Seg (len t) & len t = n ) by A1, Def1, FINSEQ_1:def 3;
A5: for k being Nat st k in dom t holds
t . k = (Line (A,1)) . k

proof

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

end;

len (Line (A,1)) = n by A3, MATRIX_1:def 7;
then dom (Line (A,1)) = dom t by A4, FINSEQ_1:def 3;
hence t = Line (A,1) by A5, FINSEQ_1:13; :: thesis: verum