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

now

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 5
.= - ((f . v,w) *' ) by COMPLFLD:88
.= - ((f *' ) . v,w) by Def8
.= (- (f *' )) . v,w by BILINEAR:def 5 ; :: thesis: verum

end;

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