theorem
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)))))