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

A1: now

let k9 be set ; :: thesis: ( k9 in dom ((f + g) *' ) implies ((f + g) *' ) . k9 = ((f *' ) + (g *' )) . k9 )
assume k9 in dom ((f + g) *' ) ; :: thesis: ((f + g) *' ) . k9 = ((f *' ) + (g *' )) . k9
then reconsider k = k9 as Element of NAT ;
(f + g) . k = (f . k) + (g . k) by NORMSP_1:def 5;
then ((f + g) *' ) . k = ((power F_Complex ) . (- (1_ F_Complex )),k) * (((f . k) + (g . k)) *' ) by Def9
.= ((power F_Complex ) . (- (1_ F_Complex )),k) * (((f . k) *' ) + ((g . k) *' )) by COMPLFLD:87
.= (((power F_Complex ) . (- (1_ F_Complex )),k) * ((f . k) *' )) + (((power F_Complex ) . (- (1_ F_Complex )),k) * ((g . k) *' ))
.= ((f *' ) . k) + (((power F_Complex ) . (- (1_ F_Complex )),k) * ((g . k) *' )) by Def9
.= ((f *' ) . k) + ((g *' ) . k) by Def9 ;
hence ((f + g) *' ) . k9 = ((f *' ) + (g *' )) . k9 by NORMSP_1:def 5; :: thesis: verum

end;

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