for V, W being Z_Module
for v, u being Vector of V
for w, t being Vector of W
for f being bilinear-Form of V,W holds f . ((v - u),(w - t)) = ((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t)))