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 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:8;
A3: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:25;
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:106;
then 1 <= j by FINSEQ_1:3;
then 1 + 1 <= j + 1 by XREAL_1:8;
then A10: 1 <= j + 1 by XXREAL_0:2;
j + 1 <= n by A9, INT_1:20;
then A11: l in Seg n by A7, A10;
i in Seg n by A5, ZFMISC_1:106;
then 1 <= i by FINSEQ_1:3;
then 1 + 1 <= i + 1 by XREAL_1:8;
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, Def10;
i + 1 <= n by A8, INT_1:20;
then k in Seg n by A6, A12;
then [k,l] in Indices M1 by A3, A11, ZFMISC_1:106;
then M1 * k,l = p . (((l - k) mod (len p)) + 1) by A6, A7, A13, A2, Def9
.= p . (((j - i) mod (len p)) + 1) by A6, A7
.= M1 * i,j by A1, A5, A13, A3, Def9 ;
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:8;
A16: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:25;
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:106;
then 1 <= j by FINSEQ_1:3;
then 1 + 1 <= j + 1 by XREAL_1:8;
then A23: 1 <= j + 1 by XXREAL_0:2;
j + 1 <= n by A22, INT_1:20;
then A24: l in Seg n by A20, A23;
i in Seg n by A18, ZFMISC_1:106;
then 1 <= i by FINSEQ_1:3;
then 1 + 1 <= i + 1 by XREAL_1:8;
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, Def10;
i + 1 <= n by A21, INT_1:20;
then k in Seg n by A19, A25;
then [k,l] in Indices M1 by A16, A24, ZFMISC_1:106;
then M1 * k,l = (- p) . (((l - k) mod (len p)) + 1) by A19, A20, A26, A15, Def9
.= (- p) . (((j - i) mod (len p)) + 1) by A19, A20
.= M1 * i,j by A14, A18, A26, A16, Def9 ;
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