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 12
.= (r *' ) * ((f . v) *' ) by COMPLFLD:90
.= (r *' ) * ((f *' ) . v) by Def2 ; :: thesis: verum