for V, W being Z_Module
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of INT.Ring
for f being bilinear-FrForm of V,W holds f . ((v - (a * u)),(w - (b * t))) = ((f . (v,w)) - (b * (f . (v,t)))) - ((a * (f . (u,w))) - (a * (b * (f . (u,t)))))