let V be non empty VectSpStr of 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:83 ; :: thesis: verum