let V, W be non empty ModuleStr over F_Complex ; :: thesis: for f, g being Form of V,W holds (f - g) *' = (f *') - (g *')
let f, g be Form of V,W; :: thesis: (f - g) *' = (f *') - (g *')
thus (f - g) *' = (f *') + ((- g) *') by Th31
.= (f *') - (g *') by Th32 ; :: thesis: verum