theorem Th3: :: MATRIX13:3

for n being Nat
for K being Field
for M being Matrix of n,K holds diagonal_of_Matrix M = diagonal_of_Matrix (M @)