let w be Vector of W; :: according to BILINEAR:def 14 :: thesis: FunctionalSAF ((a * f),w) is homogeneous

set Ffg = FunctionalSAF ((a * f),w);

set Ff = FunctionalSAF (f,w);

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

let b be Scalar of ; :: thesis: (FunctionalSAF ((a * f),w)) . (b * v) = b * ((FunctionalSAF ((a * f),w)) . v)

thus (FunctionalSAF ((a * f),w)) . (b * v) = (a * (FunctionalSAF (f,w))) . (b * v) by Th14

.= a * ((FunctionalSAF (f,w)) . (b * v)) by HAHNBAN1:def 6

.= a * (b * ((FunctionalSAF (f,w)) . v)) by HAHNBAN1:def 8

.= b * (a * ((FunctionalSAF (f,w)) . v)) by GROUP_1:def 3

.= b * ((a * (FunctionalSAF (f,w))) . v) by HAHNBAN1:def 6

.= b * ((FunctionalSAF ((a * f),w)) . v) by Th14 ; :: thesis: verum

set Ffg = FunctionalSAF ((a * f),w);

set Ff = FunctionalSAF (f,w);

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

let b be Scalar of ; :: thesis: (FunctionalSAF ((a * f),w)) . (b * v) = b * ((FunctionalSAF ((a * f),w)) . v)

thus (FunctionalSAF ((a * f),w)) . (b * v) = (a * (FunctionalSAF (f,w))) . (b * v) by Th14

.= a * ((FunctionalSAF (f,w)) . (b * v)) by HAHNBAN1:def 6

.= a * (b * ((FunctionalSAF (f,w)) . v)) by HAHNBAN1:def 8

.= b * (a * ((FunctionalSAF (f,w)) . v)) by GROUP_1:def 3

.= b * ((a * (FunctionalSAF (f,w))) . v) by HAHNBAN1:def 6

.= b * ((FunctionalSAF ((a * f),w)) . v) by Th14 ; :: thesis: verum