let i, j, k, n, 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 :: thesis: ( ( i <= j & ( 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) ) ) or ( i >= j & ( 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) ) ) )

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

case A1: 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) )

then A2: i + 1 <= j + 1 by XREAL_1:6;
A3: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_0:24;
assume that
A4: M1 is anti-circular and
A5: [i,j] in [:(Seg n),(Seg n):] and
A6: k = i + 1 and
A7: l = j + 1 and
A8: i < n and
A9: 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) )
j in Seg n by A5, ZFMISC_1:87;
then 1 <= j by FINSEQ_1:1;
then 1 + 1 <= j + 1 by XREAL_1:6;
then A10: 1 <= j + 1 by XXREAL_0:2;
j + 1 <= n by A9, INT_1:7;
then A11: l in Seg n by A7, A10;
i in Seg n by A5, ZFMISC_1:87;
then 1 <= i by FINSEQ_1:1;
then 1 + 1 <= i + 1 by XREAL_1:6;
then A12: 1 <= i + 1 by XXREAL_0:2;
consider p being FinSequence of K such that
len p = width M1 and
A13: M1 is_anti-circular_about p by A4;
i + 1 <= n by A8, INT_1:7;
then k in Seg n by A6, A12;
then [k,l] in Indices M1 by A3, A11, ZFMISC_1:87;
then M1 * (k,l) = p . (((l - k) mod (len p)) + 1) by A6, A7, A13, A2
.= p . (((j - i) mod (len p)) + 1) by A6, A7
.= M1 * (i,j) by A1, A5, A13, A3 ;
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 A14: 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) )

then A15: i + 1 >= j + 1 by XREAL_1:6;
A16: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_0:24;
assume that
A17: M1 is anti-circular and
A18: [i,j] in [:(Seg n),(Seg n):] and
A19: k = i + 1 and
A20: l = j + 1 and
A21: i < n and
A22: 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) )
j in Seg n by A18, ZFMISC_1:87;
then 1 <= j by FINSEQ_1:1;
then 1 + 1 <= j + 1 by XREAL_1:6;
then A23: 1 <= j + 1 by XXREAL_0:2;
j + 1 <= n by A22, INT_1:7;
then A24: l in Seg n by A20, A23;
i in Seg n by A18, ZFMISC_1:87;
then 1 <= i by FINSEQ_1:1;
then 1 + 1 <= i + 1 by XREAL_1:6;
then A25: 1 <= i + 1 by XXREAL_0:2;
consider p being FinSequence of K such that
len p = width M1 and
A26: M1 is_anti-circular_about p by A17;
i + 1 <= n by A21, INT_1:7;
then k in Seg n by A19, A25;
then [k,l] in Indices M1 by A16, A24, ZFMISC_1:87;
then M1 * (k,l) = (- p) . (((l - k) mod (len p)) + 1) by A19, A20, A26, A15
.= (- p) . (((j - i) mod (len p)) + 1) by A19, A20
.= M1 * (i,j) by A14, A18, A26, A16 ;
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