let v be Vector of V; :: according to HERMITAN:def 4 :: thesis: 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; :: according to HERMITAN:def 1 :: thesis: 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 ; :: thesis: (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 ;

:: thesis: verum

set fg = FormFunctional (f,g);

set F = FunctionalFAF ((FormFunctional (f,g)),v);

let y be Vector of W; :: according to HERMITAN:def 1 :: thesis: 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 ; :: thesis: (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 ;

:: thesis: verum