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 that
A1: A is col_circulant and
A2: [i,j] in [:(Seg n),(Seg n):] and
A3: k = i + 1 and
A4: l = j + 1 and
A5: i < n and
A6: j < n ; :: thesis: A * i,j = A * k,l
A7: [i,j] in Indices A by A2, MATRIX_1:25;
j in Seg n by A2, ZFMISC_1:106;
then 1 <= j by FINSEQ_1:3;
then 1 + 1 <= j + 1 by XREAL_1:8;
then A8: 1 <= l by A4, XXREAL_0:2;
l <= n by A4, A6, INT_1:20;
then A9: l in Seg n by A8;
i in Seg n by A2, ZFMISC_1:106;
then 1 <= i by FINSEQ_1:3;
then 1 + 1 <= i + 1 by XREAL_1:8;
then A10: 1 <= k by A3, XXREAL_0:2;
consider p being FinSequence of D such that
len p = len A and
A11: A is_col_circulant_about p by A1, Def5;
k <= n by A3, A5, INT_1:20;
then ( Indices A = [:(Seg n),(Seg n):] & k in Seg n ) by A10, MATRIX_1:25;
then [k,l] in Indices A by A9, ZFMISC_1:106;
then A * k,l = p . (((k - l) mod (len p)) + 1) by A11, Def4
.= p . (((i - j) mod (len p)) + 1) by A3, A4
.= A * i,j by A11, A7, Def4 ;
hence A * i,j = A * k,l ; :: thesis: verum