let n be Nat; :: thesis: 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; :: thesis: 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; :: 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 :: thesis: for v being Vector of (ker (f |^ n)) holds (fK |^ n) . v = 0. (ker (f |^ n))
let v be Vector of (ker (f |^ n)); :: thesis: (fK |^ n) . v = 0. (ker (f |^ n))
reconsider v1 = v as Vector of V by VECTSP_4:10;
A1: v1 in ker (f |^ n) ;
thus (fK |^ n) . v = ((f |^ n) | (ker (f |^ n))) . v by VECTSP11:22
.= (f |^ n) . v1 by FUNCT_1:49
.= 0. V by A1, RANKNULL:10
.= 0. (ker (f |^ n)) by VECTSP_4:11 ; :: thesis: verum
end;
hence f | (ker (f |^ n)) is nilpotent linear-transformation of (ker (f |^ n)),(ker (f |^ n)) by Def4; :: thesis: verum