theorem Th11: :: MATRIXJ2:11

for n being Nat
for K being Field
for L being Element of K holds <*(Jordan_block (L,n))*> is FinSequence_of_Jordan_block of L,K