theorem Th42: :: HERMITAN:42

for V being VectSp of F_Complex
for v, w being Vector of V
for f being sesquilinear-Form of V,V
for r being Real
for a being Element of F_Complex st |.a.| = 1 holds
f . ((v - (([**r,0**] * a) * w)),(v - (([**r,0**] * a) * w))) = (((f . (v,v)) - ([**r,0**] * (a * (f . (w,v))))) - ([**r,0**] * ((a *') * (f . (v,w))))) + ([**(r ^2),0**] * (f . (w,w)))