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 *')

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

hence
(a * f) *' = (a *') * (f *')
by FUNCT_2:63; :: thesis: verumlet 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;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