let i, j, k, n, l be Element of NAT ; :: thesis: for D being non empty set
for A being Matrix of n,D st A is line_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 line_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 line_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 line_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)
consider p being FinSequence of D such that
len p = width A and
A7: A is_line_circulant_about p by A1;
A8: Indices A = [:(Seg n),(Seg n):] by MATRIX_0:24;
j in Seg n by A2, ZFMISC_1:87;
then 1 <= j by FINSEQ_1:1;
then 1 + 1 <= j + 1 by XREAL_1:6;
then A9: 1 <= j + 1 by XXREAL_0:2;
j + 1 <= n by A6, INT_1:7;
then A10: l in Seg n by A4, A9;
i in Seg n by A2, ZFMISC_1:87;
then 1 <= i by FINSEQ_1:1;
then 1 + 1 <= i + 1 by XREAL_1:6;
then A11: 1 <= i + 1 by XXREAL_0:2;
i + 1 <= n by A5, INT_1:7;
then k in Seg n by A3, A11;
then [k,l] in Indices A by A8, A10, ZFMISC_1:87;
then A * (k,l) = p . (((l - k) mod (len p)) + 1) by A7
.= p . (((j - i) mod (len p)) + 1) by A3, A4
.= A * (i,j) by A2, A7, A8 ;
hence A * (i,j) = A * (k,l) ; :: thesis: verum