theorem Th27: :: BILINEAR:27

for K being non empty addLoopStr
for V, W being non empty ModuleStr over K
for v being Vector of V
for u, w being Vector of W
for f being Form of V,W st f is additiveFAF holds
f . (v,(u + w)) = (f . (v,u)) + (f . (v,w))