let f be Polynomial of F_Complex; :: thesis: (- f) *' = - (f *')
set h1 = - f;
A1: now :: thesis: for k9 being object st k9 in dom ((- f) *') holds
((- f) *') . k9 = (- (f *')) . k9
let k9 be object ; :: 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:44;
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:52
.= - (((power F_Complex) . ((- (1_ F_Complex)),k)) * ((f . k) *')) by VECTSP_1:8
.= - ((f *') . k) by Def9 ;
hence ((- f) *') . k9 = (- (f *')) . k9 by BHSP_1:44; :: 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:2; :: thesis: verum