let V be non empty ModuleStr over F_Complex ; :: thesis: for f being Functional of V
for a being Scalar of holds (a * f) *' = (a *') * (f *')
let f be Functional of V; :: thesis: for a being Scalar of holds (a * f) *' = (a *') * (f *')
let a be Scalar of ; :: thesis: (a * f) *' = (a *') * (f *')

now :: thesis: for v being Vector of V holds ((a * f) *') . v = ((a *') * (f *')) . v

let v be Vector of V; :: thesis: ((a * f) *') . v = ((a *') * (f *')) . v
thus ((a * f) *') . v = ((a * f) . v) *' by Def2
.= (a * (f . v)) *' by HAHNBAN1:def 6
.= (a *') * ((f . v) *') by COMPLFLD:54
.= (a *') * ((f *') . v) by Def2
.= ((a *') * (f *')) . v by HAHNBAN1:def 6 ; :: thesis: verum

end;

hence (a * f) *' = (a *') * (f *') by FUNCT_2:63; :: thesis: verum