theorem Th38:
for
V,
W being
VectSp of
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)))))