:: deftheorem Def5 defines UnionKers VECTSP11:def 5 :
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for b₄ being strict Subspace of V1 holds
( b₄ = UnionKers f iff the carrier of b₄ = { v where v is Vector of V1 : ex n being Nat st (f |^ n) . v = 0. V1 } );