theorem
for
K being non
empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr for
V,
W being
VectSp of
K for
v,
u being
Vector of
V for
w,
t being
Vector of
W for
a,
b being
Element of
K for
f being
bilinear-Form 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)))))