:: deftheorem Def2 defines Jordan-block-yielding MATRIXJ2:def 2 :
for K being Field
for G being FinSequence of ( the carrier of K *) * holds
( G is Jordan-block-yielding iff for i being Nat st i in dom G holds
ex L being Element of K ex n being Nat st G . i = Jordan_block (L,n) );