:: deftheorem defines - BILINEAR:def 6 :
for K being non empty addLoopStr
for V, W being non empty ModuleStr over K
for f, g being Form of V,W holds f - g = f + (- g);