let x be Vector of V; :: according to HAHNBAN1:def 8 :: thesis: for r being Scalar of holds (v * f) . (r * x) = r * ((v * f) . x)
let r be Scalar of ; :: thesis: (v * f) . (r * x) = r * ((v * f) . x)
thus (v * f) . (r * x) = v * (f . (r * x)) by Def6
.= v * (r * (f . x)) by Def8
.= r * (v * (f . x)) by GROUP_1:def 3
.= r * ((v * f) . x) by Def6 ; :: thesis: verum