:: deftheorem defines NulForm BILINEAR:def 1 :
for K being non empty ZeroStr
for V, W being ModuleStr over K holds NulForm (V,W) = [: the carrier of V, the carrier of W:] --> (0. K);