let V be non empty ModuleStr over F_Complex ; :: thesis: for f being Functional of V
for v being Vector of V holds (FormFunctional (f,(f *'))) . (v,v) = |.(f . v).| ^2
let f be Functional of V; :: thesis: for v being Vector of V holds (FormFunctional (f,(f *'))) . (v,v) = |.(f . v).| ^2
let v be Vector of V; :: thesis: (FormFunctional (f,(f *'))) . (v,v) = |.(f . v).| ^2
set g = FormFunctional (f,(f *'));
thus (FormFunctional (f,(f *'))) . (v,v) = (f . v) * ((f *') . v) by BILINEAR:def 10
.= (f . v) * ((f . v) *') by Def2
.= |.(f . v).| ^2 by Th13 ; :: thesis: verum