let v be Vector of V; :: according to HERMITAN:def 1 :: thesis: for a being Scalar of holds (f *') . (a * v) = (a *') * ((f *') . v)
let r be Scalar of ; :: thesis: (f *') . (r * v) = (r *') * ((f *') . v)
thus (f *') . (r * v) = (f . (r * v)) *' by Def2
.= (r * (f . v)) *' by HAHNBAN1:def 8
.= (r *') * ((f . v) *') by COMPLFLD:54
.= (r *') * ((f *') . v) by Def2 ; :: thesis: verum