:: deftheorem Def3 defines FinSequence_of_Jordan_block MATRIXJ2:def 3 :
for K being Field
for L being Element of K
for b₃ being FinSequence_of_Jordan_block of K holds
( b₃ is FinSequence_of_Jordan_block of L,K iff for i being Nat st i in dom b₃ holds
ex n being Nat st b₃ . i = Jordan_block (L,n) );