let V, W be non empty VectSpStr of 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 Th34
.= (f *') - (g *') by Th35 ; :: thesis: verum