let M1 be Matrix of n,K; ( M1 is symmetric & M1 is subsymmetric implies M1 is central_symmetric )
assume that
A1:
M1 is symmetric
and
A2:
M1 is subsymmetric
; M1 is central_symmetric
A3:
Indices M1 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
let i, j, k, l be Nat; MATRIX17:def 3 ( [i,j] in Indices M1 & k = (n + 1) - i & l = (n + 1) - j implies M1 * (i,j) = M1 * (k,l) )
assume that
A4:
[i,j] in Indices M1
and
A5:
( k = (n + 1) - i & l = (n + 1) - j )
; M1 * (i,j) = M1 * (k,l)
( k in Seg n & l in Seg n )
by A3, A4, A5, Lm2;
then A6:
( [k,l] in [:(Seg n),(Seg n):] & [l,k] in [:(Seg n),(Seg n):] )
by ZFMISC_1:87;
thus M1 * (i,j) =
M1 * (l,k)
by A2, A4, A5
.=
(M1 @) * (k,l)
by A6, A3, MATRIX_0:def 6
.=
M1 * (k,l)
by A1
; verum