:: deftheorem Def11 defines Ker VECTSP10:def 11 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being VectSp of K
for f being linear-Functional of V
for b₄ being non empty strict Subspace of V holds
( b₄ = Ker f iff the carrier of b₄ = ker f );