theorem Th37:
for
V,
W being non
empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over
F_Complex for
v,
u being
Vector of
V for
w,
t being
Vector of
W for
a,
b being
Element of
F_Complex for
f being
sesquilinear-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)))))