let w be Vector of W; :: according to ZMATRLIN:def 25 :: 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₁ being Element of the carrier of INT.Ring holds (FunctionalSAF ((a * f),w)) . (b₁ * v) = b₁ * ((FunctionalSAF ((a * f),w)) . v)
let b be Element of INT.Ring; :: 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 BLTh14
.= 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))
.= b * ((a * (FunctionalSAF (f,w))) . v) by HAHNBAN1:def 6
.= b * ((FunctionalSAF ((a * f),w)) . v) by BLTh14 ; :: thesis: verum