:: deftheorem defines - BILINEAR:def 5 :
for K being non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr
for V, W being non empty ModuleStr over K
for f being Form of V,W holds - f = (- (1. K)) * f;