theorem Th2: :: MATRTOP3:2

for n being Nat
for K being Field
for M being diagonal Matrix of n,K holds M @ = M