:: deftheorem Def18 defines LKer BILINEAR:def 18 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being VectSp of K
for W being non empty ModuleStr over K
for f being additiveSAF homogeneousSAF Form of V,W
for b₅ being non empty strict Subspace of V holds
( b₅ = LKer f iff the carrier of b₅ = leftker f );