let f be Polynomial of F_Complex ; :: thesis: (- f) *' = - (f *' )
set h1 = - f;
A1: dom ((- f) *' ) = NAT by FUNCT_2:def 1
.= dom (- (f *' )) by FUNCT_2:def 1 ;

now

let k' be set ; :: thesis: ( k' in dom ((- f) *' ) implies ((- f) *' ) . k' = (- (f *' )) . k' )
assume k' in dom ((- f) *' ) ; :: thesis: ((- f) *' ) . k' = (- (f *' )) . k'
then reconsider k = k' 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) *' ) . k' = (- (f *' )) . k' by BHSP_1:def 10; :: thesis: verum

end;

hence (- f) *' = - (f *' ) by A1, FUNCT_1:9; :: thesis: verum