let y be Vector of W; :: according to BILINEAR:def 14 :: thesis: FunctionalSAF ((FormFunctional (f,g)),y) is homogeneous

set fg = FormFunctional (f,g);

set F = FunctionalSAF ((FormFunctional (f,g)),y);

let v be Vector of V; :: according to HAHNBAN1:def 8 :: thesis: for b_{1} being Element of the carrier of K holds (FunctionalSAF ((FormFunctional (f,g)),y)) . (b_{1} * v) = b_{1} * ((FunctionalSAF ((FormFunctional (f,g)),y)) . v)

let r be Scalar of ; :: thesis: (FunctionalSAF ((FormFunctional (f,g)),y)) . (r * v) = r * ((FunctionalSAF ((FormFunctional (f,g)),y)) . v)

A1: FunctionalSAF ((FormFunctional (f,g)),y) = (g . y) * f by Th25;

hence (FunctionalSAF ((FormFunctional (f,g)),y)) . (r * v) = (g . y) * (f . (r * v)) by HAHNBAN1:def 6

.= (g . y) * (r * (f . v)) by HAHNBAN1:def 8

.= r * ((g . y) * (f . v)) by GROUP_1:def 3

.= r * ((FunctionalSAF ((FormFunctional (f,g)),y)) . v) by A1, HAHNBAN1:def 6 ;

:: thesis: verum

set fg = FormFunctional (f,g);

set F = FunctionalSAF ((FormFunctional (f,g)),y);

let v be Vector of V; :: according to HAHNBAN1:def 8 :: thesis: for b

let r be Scalar of ; :: thesis: (FunctionalSAF ((FormFunctional (f,g)),y)) . (r * v) = r * ((FunctionalSAF ((FormFunctional (f,g)),y)) . v)

A1: FunctionalSAF ((FormFunctional (f,g)),y) = (g . y) * f by Th25;

hence (FunctionalSAF ((FormFunctional (f,g)),y)) . (r * v) = (g . y) * (f . (r * v)) by HAHNBAN1:def 6

.= (g . y) * (r * (f . v)) by HAHNBAN1:def 8

.= r * ((g . y) * (f . v)) by GROUP_1:def 3

.= r * ((FunctionalSAF ((FormFunctional (f,g)),y)) . v) by A1, HAHNBAN1:def 6 ;

:: thesis: verum