theorem :: MATRIXJ2:27

for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for J being FinSequence_of_Jordan_block of 0. K,K
for M being Matrix of len b1, len b1,K st M = block_diagonal (J,(0. K)) & len b1 > 0 holds
for F being nilpotent Function of V1,V1 st F = Mx2Tran (M,b1,b1) holds
( ex i being Nat st
( i in dom J & len (J . i) = deg F ) & ( for i being Nat st i in dom J holds
len (J . i) <= deg F ) )