theorem :: HERMITAN:17

for V being non empty ModuleStr over F_Complex holds (0Functional V) *' = 0Functional V