let w be Vector of W; :: according to ZMODLAT1:def 30 :: thesis: FrFunctionalSAF ((a * f),w) is homogeneous
set Ffg = FrFunctionalSAF ((a * f),w);
set Ff = FrFunctionalSAF (f,w);
let v be Vector of V; :: according to ZMODLAT1:def 22 :: thesis: for r being Scalar of holds (FrFunctionalSAF ((a * f),w)) . (r * v) = r * ((FrFunctionalSAF ((a * f),w)) . v)
let b be Scalar of ; :: thesis: (FrFunctionalSAF ((a * f),w)) . (b * v) = b * ((FrFunctionalSAF ((a * f),w)) . v)
thus (FrFunctionalSAF ((a * f),w)) . (b * v) = (a * (FrFunctionalSAF (f,w))) . (b * v) by HTh14
.= a * ((FrFunctionalSAF (f,w)) . (b * v)) by HDef6
.= a * (b * ((FrFunctionalSAF (f,w)) . v)) by HDef8
.= b * (a * ((FrFunctionalSAF (f,w)) . v))
.= b * ((a * (FrFunctionalSAF (f,w))) . v) by HDef6
.= b * ((FrFunctionalSAF ((a * f),w)) . v) by HTh14 ; :: thesis: verum