:: deftheorem Def2 defines *' HERMITAN:def 2 :
for V being non empty ModuleStr over F_Complex
for f, b₃ being Functional of V holds
( b₃ = f *' iff for v being Vector of V holds b₃ . v = (f . v) *' );