let w be Vector of V; :: according to BILINEAR:def 14 :: thesis: FunctionalFAF ((a * f),w) is homogeneous
set Ffg = FunctionalFAF ((a * f),w);
set Ff = FunctionalFAF (f,w);
let v be Vector of W; :: according to HAHNBAN1:def 12 :: thesis: for b₁ being Element of the carrier of K holds (FunctionalFAF ((a * f),w)) . (b₁ * v) = b₁ * ((FunctionalFAF ((a * f),w)) . v)
let b be Scalar of ; :: thesis: (FunctionalFAF ((a * f),w)) . (b * v) = b * ((FunctionalFAF ((a * f),w)) . v)
thus (FunctionalFAF ((a * f),w)) . (b * v) = (a * (FunctionalFAF (f,w))) . (b * v) by Th16
.= a * ((FunctionalFAF (f,w)) . (b * v)) by HAHNBAN1:def 9
.= a * (b * ((FunctionalFAF (f,w)) . v)) by HAHNBAN1:def 12
.= b * (a * ((FunctionalFAF (f,w)) . v)) by GROUP_1:def 4
.= b * ((a * (FunctionalFAF (f,w))) . v) by HAHNBAN1:def 9
.= b * ((FunctionalFAF ((a * f),w)) . v) by Th16 ; :: thesis: verum