let i, j, n, k, l be Element of NAT ; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
M1 * k,l = M1 * i,j
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
M1 * k,l = M1 * i,j
let M1 be Matrix of n,K; :: thesis: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * k,l = M1 * i,j )

now

per cases ( i <= j or i >= j ) ;

case C1: i <= j ; :: thesis: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n & M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * k,l = M1 * i,j )

assume A1: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n ) ; :: thesis: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * k,l = M1 * i,j )
consider p being FinSequence of K such that
A2: ( len p = width M1 & M1 is_anti-circular_about p ) by A1, Def11;
A4: Indices M1 = [:(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 B5: [k,l] in Indices M1 by A4, ZFMISC_1:106;
B6: i + 1 <= j + 1 by C1, XREAL_1:8;
M1 * k,l = p . (((l - k) mod (len p)) + 1) by A1, B5, B6, A2, Def10
.= p . (((j - i) mod (len p)) + 1) by A1
.= M1 * i,j by C1, A1, A4, A2, Def10 ;
hence ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * k,l = M1 * i,j ) ; :: thesis: verum

end;

case C2: i >= j ; :: thesis: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n & M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * k,l = M1 * i,j )

assume A1: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n ) ; :: thesis: ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * k,l = M1 * i,j )
consider p being FinSequence of K such that
A2: ( len p = width M1 & M1 is_anti-circular_about p ) by A1, Def11;
A4: Indices M1 = [:(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 B5: [k,l] in Indices M1 by A4, ZFMISC_1:106;
B6: i + 1 >= j + 1 by C2, XREAL_1:8;
M1 * k,l = (- p) . (((l - k) mod (len p)) + 1) by A1, B6, B5, A2, Def10
.= (- p) . (((j - i) mod (len p)) + 1) by A1
.= M1 * i,j by C2, A1, A4, A2, Def10 ;
hence ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * k,l = M1 * i,j ) ; :: thesis: verum

end;

end;

end;

hence ( M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n implies M1 * k,l = M1 * i,j ) ; :: thesis: verum