theorem Th29: :: MATRIXJ2:29

for K being Field
for V1 being finite-dimensional VectSp of K
for F being nilpotent linear-transformation of V1,V1 ex J being non-empty FinSequence_of_Jordan_block of 0. K,K ex b1 being OrdBasis of V1 st AutMt (F,b1,b1) = block_diagonal (J,(0. K))