let V be non empty ModuleStr over 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 Th18
.= (f *') - (g *') by Th19 ; :: thesis: verum