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

now

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

end;

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