theorem :: VECTSP11:35

for K being Field
for V being finite-dimensional VectSp of K
for f being linear-transformation of V,V
for n being Nat st UnionKers f = ker (f |^ n) holds
V is_the_direct_sum_of ker (f |^ n), im (f |^ n)