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