theorem Th18: :: MATRIXJ2:18

for n being Nat
for K being Field
for V being VectSp of K
for W being Subspace of V
for f being nilpotent linear-transformation of V,V
for fI being nilpotent Function of (im (f |^ n)),(im (f |^ n)) st fI = f | (im (f |^ n)) & n <= deg f holds
(deg fI) + n = deg f