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 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, Def2;
A8: Indices A = [:(Seg n),(Seg n):] by 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 A9: 1 <= j + 1 by XXREAL_0:2;
j + 1 <= n by A6, INT_1:20;
then A10: l in Seg n by A4, A9;
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 A11: 1 <= i + 1 by XXREAL_0:2;
i + 1 <= n by A5, INT_1:20;
then k in Seg n by A3, A11;
then [k,l] in Indices A by A8, A10, ZFMISC_1:106;
then A * k,l = p . (((l - k) mod (len p)) + 1) by A7, Def1
.= p . (((j - i) mod (len p)) + 1) by A3, A4
.= A * i,j by A2, A7, A8, Def1 ;
hence A * i,j = A * k,l ; :: thesis: verum