let v be Vector of V; ZMATRLIN:def 24 FunctionalFAF ((FormFunctional (f,g)),v) is homogeneous
set fg = FormFunctional (f,g);
set F = FunctionalFAF ((FormFunctional (f,g)),v);
let y be Vector of W; HAHNBAN1:def 8 for b1 being Element of the carrier of INT.Ring holds (FunctionalFAF ((FormFunctional (f,g)),v)) . (b1 * y) = b1 * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y)
let r be Element of INT.Ring; (FunctionalFAF ((FormFunctional (f,g)),v)) . (r * y) = r * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y)
A1:
FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g
by BLTh24;
hence (FunctionalFAF ((FormFunctional (f,g)),v)) . (r * y) =
(f . v) * (g . (r * y))
by HAHNBAN1:def 6
.=
(f . v) * (r * (g . y))
by HAHNBAN1:def 8
.=
r * ((f . v) * (g . y))
.=
r * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y)
by A1, HAHNBAN1:def 6
;
verum