let V be non empty VectSpStr of 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

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

end;

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