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

now

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

end;

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