let V be non empty VectSpStr of 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 11
.= (f . v) * ((f . v) *' ) by Def2
.= |.(f . v).| ^2 by Th16 ; :: thesis: verum