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 Th28, COMPLEX1:13;
then Re ((FormFunctional (f,(f *'))) . (v,v)) = |.(f . v).| ^2 by COMPLEX1:77;
hence 0 <= Re ((FormFunctional (f,(f *'))) . (v,v)) by XREAL_1:63; :: 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 10
.= (((f . v) * ((f . w) *')) *') *' by Def2
.= (((f . v) *') * (((f . w) *') *')) *' by COMPLFLD:54
.= ((f . w) * ((f *') . v)) *' by Def2
.= ((FormFunctional (f,(f *'))) . (w,v)) *' by BILINEAR:def 10 ; :: 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 Th28, COMPLEX1:13;
hence Im ((FormFunctional (f,(f *'))) . (v,v)) = 0 by COMPLEX1:77; :: thesis: verum