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 A1: ( A is_line_circulant_about t & n > 0 ) ; :: thesis: t = Line A,1
A3: ( len A = n & width A = n ) by MATRIX_1:25;
then A4: ( len (Line A,1) = n & dom t = Seg (len t) & len t = n ) by A1, Def1, FINSEQ_1:def 3, MATRIX_1:def 8;
then A5: dom (Line A,1) = dom t by FINSEQ_1:def 3;
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 B1: k in dom t ; :: thesis: t . k = (Line A,1) . k
then B3: k in Seg (width A) by A4, MATRIX_1:def 8;
n >= 0 + 1 by A1, INT_1:20;
then B5: 1 in Seg n ;
B7: ( 1 <= k & k <= n ) by B1, A4, FINSEQ_1:3;
[1,k] in [:(Seg n),(Seg n):] by B1, A4, B5, ZFMISC_1:def 2;
then B8: [1,k] in Indices A by MATRIX_1:25;
(Line A,1) . k = A * 1,k by B3, MATRIX_1:def 8
.= t . (((k - 1) mod (len t)) + 1) by A1, Def1, B8
.= t . (((k - 1) mod n) + 1) by A1, Def1, A3
.= t . ((k - 1) + 1) by B7, Lm1 ;
hence t . k = (Line A,1) . k ; :: thesis: verum

end;

hence t = Line A,1 by A5, FINSEQ_1:17; :: thesis: verum