theorem Th22: :: HERMITAN:22

for V being non empty ModuleStr over F_Complex
for f being Functional of V
for v being Vector of V holds
( f . v = 0. F_Complex iff (f *') . v = 0. F_Complex )