let i 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 UnionKers f
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 UnionKers f
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1 holds ker (f |^ i) is Subspace of UnionKers f
let f be linear-transformation of V1,V1; :: thesis: ker (f |^ i) is Subspace of UnionKers f
the carrier of (ker (f |^ i)) c= the carrier of (UnionKers f)

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 (UnionKers f) )
assume x in the carrier of (ker (f |^ i)) ; :: thesis: x in the carrier of (UnionKers f)
then reconsider v = x as Element of (ker (f |^ i)) ;
( (f |^ i) . v = 0. V1 & v is Vector of V1 ) by RANKNULL:14, VECTSP_4:10;
then x in UnionKers f by Th24;
hence x in the carrier of (UnionKers f) ; :: thesis: verum

end;

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