let w be Vector of W; ZMATRLIN:def 25 FunctionalSAF ((a * f),w) is homogeneous
set Ffg = FunctionalSAF ((a * f),w);
set Ff = FunctionalSAF (f,w);
let v be Vector of V; HAHNBAN1:def 8 for b1 being Element of the carrier of INT.Ring holds (FunctionalSAF ((a * f),w)) . (b1 * v) = b1 * ((FunctionalSAF ((a * f),w)) . v)
let b be Element of INT.Ring; (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
; verum