theorem Th27: :: HERMITAN:27

for V, W being non empty ModuleStr over F_Complex
for v being Vector of V
for w being Vector of W
for a being Element of F_Complex
for f being Form of V,W st f is cmplxhomogeneousFAF holds
f . (v,(a * w)) = (a *') * (f . (v,w))