let M1 be Matrix of n,K; :: thesis: ( M1 is symmetric & M1 is subsymmetric implies M1 is central_symmetric )
assume that
A1: M1 is symmetric and
A2: M1 is subsymmetric ; :: thesis: M1 is central_symmetric
A3: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_0:24;
let i, j, k, l be Nat; :: according to MATRIX17:def 3 :: thesis: ( [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 ) ; :: thesis: 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 ; :: thesis: verum