let V be non empty ModuleStr over F_Complex ; :: thesis: for f being Functional of V holds FormFunctional (f,(0Functional V)) is hermitan
let f be Functional of V; :: thesis: FormFunctional (f,(0Functional V)) is hermitan
let v1, w be Vector of V; :: according to HERMITAN:def 5 :: thesis: (FormFunctional (f,(0Functional V))) . (v1,w) = ((FormFunctional (f,(0Functional V))) . (w,v1)) *'
set 0F = 0Functional V;
set F = FormFunctional (f,(0Functional V));
thus (FormFunctional (f,(0Functional V))) . (v1,w) = 0. F_Complex by Lm2
.= ((FormFunctional (f,(0Functional V))) . (w,v1)) *' by Lm2, COMPLFLD:47 ; :: thesis: verum