let n be Nat; :: thesis: for K being Field
for V being VectSp of
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; :: thesis: for V being VectSp of
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 ; :: thesis: 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; :: thesis: 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;

now

let v be Vector of ; :: thesis: (fK |^ n) . v = 0. (ker (f |^ n))
reconsider v1 = v as Vector of by VECTSP_4:18;
A1: v1 in ker (f |^ n) by STRUCT_0:def 5;
thus (fK |^ n) . v = ((f |^ n) | (ker (f |^ n))) . v by VECTSP11:22
.= (f |^ n) . v1 by FUNCT_1:72
.= 0. V by A1, RANKNULL:10
.= 0. (ker (f |^ n)) by VECTSP_4:19 ; :: thesis: verum

end;

hence f | (ker (f |^ n)) is nilpotent linear-transformation of ker (f |^ n), ker (f |^ n) by Def4; :: thesis: verum