let M be Matrix of n,K; ( M = (n,n) --> a implies M is central_symmetric )
assume A1:
M = (n,n) --> a
; M is central_symmetric
let i, j, k, l be Nat; MATRIX17:def 3 ( [i,j] in Indices M & k = (n + 1) - i & l = (n + 1) - j implies M * (i,j) = M * (k,l) )
assume that
A2:
[i,j] in Indices M
and
A3:
( k = (n + 1) - i & l = (n + 1) - j )
; M * (i,j) = M * (k,l)
A4:
Indices M = [:(Seg n),(Seg n):]
by MATRIX_0:24;
( k in Seg n & l in Seg n )
by A3, A2, A4, Lm2;
then
[k,l] in [:(Seg n),(Seg n):]
by ZFMISC_1:87;
then
M * (k,l) = a
by A1, A4, MATRIX_0:46;
hence
M * (i,j) = M * (k,l)
by A1, A2, MATRIX_0:46; verum