let v be Vector of V; :: according to HAHNBAN1:def 8 :: 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:54
.= r * ((f *') . v) by Def2 ; :: thesis: verum