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