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 *' )
thus (f - g) *' = (f *' ) + ((- g) *' ) by Th21
.= (f *' ) - (g *' ) by Th22 ; :: thesis: verum