let i, j, n, k, l be Element of NAT ; :: thesis: for D being non empty set
for A being Matrix of n,D st A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * i,j = A * k,l
let D be non empty set ; :: thesis: for A being Matrix of n,D st A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * i,j = A * k,l
let A be Matrix of n,D; :: thesis: ( A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies A * i,j = A * k,l )
assume A1: ( A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n ) ; :: thesis: A * i,j = A * k,l
consider p being FinSequence of D such that
A2: ( len p = len A & A is_col_circulant_about p ) by A1, Def5;
A4: Indices A = [:(Seg n),(Seg n):] by MATRIX_1:25;
B1: [i,j] in Indices A by A1, MATRIX_1:25;
( i in Seg n & j in Seg n ) by A1, ZFMISC_1:106;
then B3: ( 1 <= i & i <= n & 1 <= j & j <= n ) by FINSEQ_1:3;
( 1 + 1 <= i + 1 & 1 + 1 <= j + 1 ) by B3, XREAL_1:8;
then ( 1 <= k & k <= n & 1 <= l & l <= n ) by A1, INT_1:20, XXREAL_0:2;
then ( k in Seg n & l in Seg n ) ;
then [k,l] in Indices A by A4, ZFMISC_1:106;
then A * k,l = p . (((k - l) mod (len p)) + 1) by A2, Def4
.= p . (((i - j) mod (len p)) + 1) by A1
.= A * i,j by B1, A2, Def4 ;
hence A * i,j = A * k,l ; :: thesis: verum