let v be Vector of V; :: according to HAHNBAN1:def 12 :: thesis: for b₁ being Element of the carrier of F_Complex holds (f *' ) . (b₁ * v) = b₁ * ((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 Def1
.= ((r *' ) *' ) * ((f . v) *' ) by COMPLFLD:90
.= r * ((f *' ) . v) by Def2 ; :: thesis: verum