let v be Vector of V; HERMITAN:def 4 FunctionalFAF ((FormFunctional (f,g)),v) is cmplxhomogeneous
set fg = FormFunctional (f,g);
set F = FunctionalFAF ((FormFunctional (f,g)),v);
let y be Vector of W; HERMITAN:def 1 for a being Scalar of holds (FunctionalFAF ((FormFunctional (f,g)),v)) . (a * y) = (a *') * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y)
let r be Scalar of ; (FunctionalFAF ((FormFunctional (f,g)),v)) . (r * y) = (r *') * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y)
A1:
FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g
by BILINEAR:24;
hence (FunctionalFAF ((FormFunctional (f,g)),v)) . (r * y) =
(f . v) * (g . (r * y))
by HAHNBAN1:def 6
.=
(f . v) * ((r *') * (g . y))
by Def1
.=
(r *') * ((f . v) * (g . y))
.=
(r *') * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y)
by A1, HAHNBAN1:def 6
;
verum