let V, W be non empty ModuleStr over F_Complex ; :: thesis: for f being Form of V,W holds (- f) *' = - (f *')
let f be Form of V,W; :: thesis: (- f) *' = - (f *')

now :: thesis: for v being Vector of V
for w being Vector of W holds ((- f) *') . (v,w) = (- (f *')) . (v,w)

let v be Vector of V; :: thesis: for w being Vector of W holds ((- f) *') . (v,w) = (- (f *')) . (v,w)
let w be Vector of W; :: thesis: ((- f) *') . (v,w) = (- (f *')) . (v,w)
thus ((- f) *') . (v,w) = ((- f) . (v,w)) *' by Def8
.= (- (f . (v,w))) *' by BILINEAR:def 4
.= - ((f . (v,w)) *') by COMPLFLD:52
.= - ((f *') . (v,w)) by Def8
.= (- (f *')) . (v,w) by BILINEAR:def 4 ; :: thesis: verum

end;

hence (- f) *' = - (f *') ; :: thesis: verum