theorem Th1: :: MATRIXJ2:1

for n being Nat
for K being Field
for L being Element of K holds diagonal_of_Matrix (Jordan_block (L,n)) = n |-> L