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

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

let v be Vector of V; :: thesis: ((- f) *') . v = (- (f *')) . v
thus ((- f) *') . v = ((- f) . v) *' by Def2
.= (- (f . v)) *' by HAHNBAN1:def 4
.= - ((f . v) *') by COMPLFLD:52
.= - ((f *') . v) by Def2
.= (- (f *')) . v by HAHNBAN1:def 4 ; :: thesis: verum

end;

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