let n be Nat; for K being Field
for V being VectSp of K
for f being linear-transformation of V,V holds f | (ker (f |^ n)) is nilpotent linear-transformation of (ker (f |^ n)),(ker (f |^ n))
let K be Field; for V being VectSp of K
for f being linear-transformation of V,V holds f | (ker (f |^ n)) is nilpotent linear-transformation of (ker (f |^ n)),(ker (f |^ n))
let V be VectSp of K; for f being linear-transformation of V,V holds f | (ker (f |^ n)) is nilpotent linear-transformation of (ker (f |^ n)),(ker (f |^ n))
let f be linear-transformation of V,V; f | (ker (f |^ n)) is nilpotent linear-transformation of (ker (f |^ n)),(ker (f |^ n))
set KER = ker (f |^ n);
reconsider fK = f | (ker (f |^ n)) as linear-transformation of (ker (f |^ n)),(ker (f |^ n)) by VECTSP11:28;
hence
f | (ker (f |^ n)) is nilpotent linear-transformation of (ker (f |^ n)),(ker (f |^ n))
by Def4; verum