set g = FormFunctional f,(f *' );
thus FormFunctional f,(f *' ) is diagReR+0valued :: thesis: ( FormFunctional f,(f *' ) is hermitan & FormFunctional f,(f *' ) is diagRvalued )

proof

let v be Vector of V; :: according to HERMITAN:def 7 :: thesis: 0 <= Re ((FormFunctional f,(f *' )) . v,v)
( (FormFunctional f,(f *' )) . v,v = (|.(f . v).| ^2 ) + (0 * <i> ) & (FormFunctional f,(f *' )) . v,v = (Re ((FormFunctional f,(f *' )) . v,v)) + ((Im ((FormFunctional f,(f *' )) . v,v)) * <i> ) ) by Th31, COMPLEX1:29;
then Re ((FormFunctional f,(f *' )) . v,v) = |.(f . v).| ^2 by COMPLEX1:163;
hence 0 <= Re ((FormFunctional f,(f *' )) . v,v) by XREAL_1:65; :: thesis: verum

end;

thus FormFunctional f,(f *' ) is hermitan :: thesis: FormFunctional f,(f *' ) is diagRvalued

proof

let v, w be Vector of V; :: according to HERMITAN:def 5 :: thesis: (FormFunctional f,(f *' )) . v,w = ((FormFunctional f,(f *' )) . w,v) *'
thus (FormFunctional f,(f *' )) . v,w = (((f . v) * ((f *' ) . w)) *' ) *' by BILINEAR:def 11
.= (((f . v) * ((f . w) *' )) *' ) *' by Def2
.= (((f . v) *' ) * (((f . w) *' ) *' )) *' by COMPLFLD:90
.= ((f . w) * ((f *' ) . v)) *' by Def2
.= ((FormFunctional f,(f *' )) . w,v) *' by BILINEAR:def 11 ; :: thesis: verum

end;

let v be Vector of V; :: according to HERMITAN:def 6 :: thesis: Im ((FormFunctional f,(f *' )) . v,v) = 0
( (FormFunctional f,(f *' )) . v,v = [**(|.(f . v).| ^2 ),0 **] & (FormFunctional f,(f *' )) . v,v = (Re ((FormFunctional f,(f *' )) . v,v)) + ((Im ((FormFunctional f,(f *' )) . v,v)) * <i> ) ) by Th31, COMPLEX1:29;
hence Im ((FormFunctional f,(f *' )) . v,v) = 0 by COMPLEX1:163; :: thesis: verum