:: deftheorem Def19 defines RKer BILINEAR:def 19 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being non empty ModuleStr over K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W
for b₅ being non empty strict Subspace of W holds
( b₅ = RKer f iff the carrier of b₅ = rightker f );