theorem Th30: :: MATRIXJ2:30

for n being Nat
for K being Field
for L being Element of K
for V being VectSp of K
for F being linear-transformation of V,V
for V1 being finite-dimensional Subspace of V
for F1 being linear-transformation of V1,V1 st V1 = ker ((F + ((- L) * (id V))) |^ n) & F | V1 = F1 holds
ex J being non-empty FinSequence_of_Jordan_block of L,K ex b1 being OrdBasis of V1 st AutMt (F1,b1,b1) = block_diagonal (J,(0. K))