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 A1:
( A is_col_circulant_about t & n > 0 )
; :: thesis: t = Col A,1
( len A = n & width A = n )
by MATRIX_1:25;
then A4:
( len (Col A,1) = n & dom t = Seg (len t) & len t = n )
by A1, Def4, FINSEQ_1:def 3, MATRIX_1:def 9;
then A5:
dom (Col A,1) = dom t
by 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 )
len (Col A,1) = len A
by MATRIX_1:def 9;
then C1:
dom (Col A,1) = Seg (len A)
by FINSEQ_1:def 3;
assume B1:
k in dom t
;
:: thesis: t . k = (Col A,1) . k
then B3:
k in dom A
by A5, C1, FINSEQ_1:def 3;
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;
[k,1] in [:(Seg n),(Seg n):]
by B1, A4, B5, ZFMISC_1:def 2;
then B8:
[k,1] in Indices A
by MATRIX_1:25;
(Col A,1) . k =
A * k,1
by B3, MATRIX_1:def 9
.=
t . (((k - 1) mod (len t)) + 1)
by A1, Def4, B8
.=
t . ((k - 1) + 1)
by A4, B7, Lm1
;
hence
t . k = (Col A,1) . k
;
:: thesis: verum
end;
hence
t = Col A,1
by A5, FINSEQ_1:17; :: thesis: verum