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

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