let n be Nat; :: thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))
let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1 holds f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))
let f be linear-transformation of V1,V1; :: thesis: f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n))
set KER = ker (f |^ n);
rng (f | (ker (f |^ n))) c= the carrier of (ker (f |^ n))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f | (ker (f |^ n))) or y in the carrier of (ker (f |^ n)) )
assume A1: y in rng (f | (ker (f |^ n))) ; :: thesis: y in the carrier of (ker (f |^ n))
consider x being set such that
A2: ( x in dom (f | (ker (f |^ n))) & (f | (ker (f |^ n))) . x = y ) by A1, FUNCT_1:def 5;
x in the carrier of (ker (f |^ n)) by A2, FUNCT_2:def 1;
then A3: x in ker (f |^ n) by STRUCT_0:def 5;
then x in V1 by VECTSP_4:17;
then reconsider v = x as Vector of V1 by STRUCT_0:def 5;
A4: dom f = the carrier of V1 by FUNCT_2:def 1;
(f |^ n) . v = 0. V1 by A3, RANKNULL:10;
then 0. V1 = (f |^ (n + 1)) . v by Th23
.= ((f |^ n) * (f |^ 1)) . v by Th20
.= ((f |^ n) * f) . v by Th19
.= (f |^ n) . (f . v) by A4, FUNCT_1:23 ;
then ( f . v in ker (f |^ n) & y = f . v ) by A2, FUNCT_1:70, RANKNULL:10;
hence y in the carrier of (ker (f |^ n)) by STRUCT_0:def 5; :: thesis: verum

end;

hence f | (ker (f |^ n)) is linear-transformation of (ker (f |^ n)),(ker (f |^ n)) by Lm1, FUNCT_2:8; :: thesis: verum