theorem :: MATRIX16:54

for i, j, k, n, l being Element of NAT
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)