theorem Th26: :: BILINEAR:26

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