let i, j be Nat; :: thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of ker (f |^ (i + j))
let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of ker (f |^ (i + j))
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of ker (f |^ (i + j))
let f be linear-transformation of V1,V1; :: thesis: ker (f |^ i) is Subspace of ker (f |^ (i + j))
the carrier of (ker (f |^ i)) c= the carrier of (ker (f |^ (i + j)))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ker (f |^ i)) or x in the carrier of (ker (f |^ (i + j))) )
assume A1: x in the carrier of (ker (f |^ i)) ; :: thesis: x in the carrier of (ker (f |^ (i + j)))
reconsider v = x as Vector of V1 by A1, VECTSP_4:10;
(f |^ i) . v = 0. V1 by A1, RANKNULL:14;
then (f |^ (i + j)) . v = 0. V1 by Th23;
then v in ker (f |^ (i + j)) by RANKNULL:10;
hence x in the carrier of (ker (f |^ (i + j))) ; :: thesis: verum

end;

hence ker (f |^ i) is Subspace of ker (f |^ (i + j)) by VECTSP_4:27; :: thesis: verum