theorem
for
V,
W being non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over
INT.Ring 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)))))