theorem :: MATRIXJ2:32

for n being Nat
for K being algebraic-closed Field
for M being Matrix of n,K ex J being non-empty FinSequence_of_Jordan_block of K ex P being Matrix of n,K st
( Sum (Len J) = n & P is invertible & M = (P * (block_diagonal (J,(0. K)))) * (P ~) )