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

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