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

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