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 A1: ( A is line_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 = width A & A is_line_circulant_about p ) by A1, Def2;
A4: Indices A = [:(Seg n),(Seg n):] by 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;
B4: ( i + 1 <= n & j + 1 <= n ) by A1, INT_1:20;
( 1 + 1 <= i + 1 & 1 + 1 <= j + 1 ) by B3, XREAL_1:8;
then ( 1 <= i + 1 & 1 <= j + 1 ) by XXREAL_0:2;
then ( k in Seg n & l in Seg n ) by A1, B4;
then [k,l] in Indices A by A4, ZFMISC_1:106;
then A * k,l = p . (((l - k) mod (len p)) + 1) by A2, Def1
.= p . (((j - i) mod (len p)) + 1) by A1
.= A * i,j by A1, A4, A2, Def1 ;
hence A * i,j = A * k,l ; :: thesis: verum