:: deftheorem defines rightker BILINEAR:def 16 :
for K being ZeroStr
for V, W being non empty ModuleStr over K
for f being Form of V,W holds rightker f = { w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K } ;