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