let f be Polynomial of F_Complex ; :: thesis: (- f) *' = - (f *' )
set h1 = - f;

A1: now

let k9 be set ; :: thesis: ( k9 in dom ((- f) *' ) implies ((- f) *' ) . k9 = (- (f *' )) . k9 )
assume k9 in dom ((- f) *' ) ; :: thesis: ((- f) *' ) . k9 = (- (f *' )) . k9
then reconsider k = k9 as Element of NAT ;
(- f) . k = - (f . k) by BHSP_1:def 10;
then ((- f) *' ) . k = ((power F_Complex ) . (- (1_ F_Complex )),k) * ((- (f . k)) *' ) by Def9
.= ((power F_Complex ) . (- (1_ F_Complex )),k) * (- ((f . k) *' )) by COMPLFLD:88
.= - (((power F_Complex ) . (- (1_ F_Complex )),k) * ((f . k) *' )) by VECTSP_1:40
.= - ((f *' ) . k) by Def9 ;
hence ((- f) *' ) . k9 = (- (f *' )) . k9 by BHSP_1:def 10; :: thesis: verum

end;

dom ((- f) *' ) = NAT by FUNCT_2:def 1
.= dom (- (f *' )) by FUNCT_2:def 1 ;
hence (- f) *' = - (f *' ) by A1, FUNCT_1:9; :: thesis: verum