let n be Element of NAT ; 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 ; 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; 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; ( 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
; t = Line (A,1)
A3:
width A = n
by MATRIX_0:24;
then A4:
( dom t = Seg (len t) & len t = n )
by A1, 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;
( k in dom t implies t . k = (Line (A,1)) . k )
assume A6:
k in dom t
;
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_0:24;
(Line (A,1)) . k =
A * (1,
k)
by A3, A4, A6, MATRIX_0:def 7
.=
t . (((k - 1) mod (len t)) + 1)
by A1, A8
.=
t . (((k - 1) mod n) + 1)
by A1, A3
.=
t . ((k - 1) + 1)
by A7, Lm1
;
hence
t . k = (Line (A,1)) . k
;
verum
end;
len (Line (A,1)) = n
by A3, MATRIX_0: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; verum