theorem :: MATRIX_6:12

for n being Nat
for R being commutative Ring
for M1, M3 being Matrix of n,R st M3 is_reverse_of M1 & n > 0 holds
M1 @ is_reverse_of M3 @