:: deftheorem Def8 defines *' HERMITAN:def 8 :
for V, W being non empty ModuleStr over F_Complex
for f, b₄ being Form of V,W holds
( b₄ = f *' iff for v being Vector of V
for w being Vector of W holds b₄ . (v,w) = (f . (v,w)) *' );