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