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

A1: now :: thesis: for k9 being object st k9 in dom ((f + g) *') holds
((f + g) *') . k9 = ((f *') + (g *')) . k9

let k9 be object ; :: 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 2;
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:51
.= (((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 2; :: 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:2; :: thesis: verum