theorem Th28: :: BILINEAR:28

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