let f be Polynomial of F_Complex; :: thesis: for z being Element of F_Complex holds (z * f) *' = (z *') * (f *')
let x be Element of F_Complex; :: thesis: (x * f) *' = (x *') * (f *')
set g1 = x * f;
set g2 = (x *') * (f *');

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

let k9 be object ; :: thesis: ( k9 in dom ((x * f) *') implies ((x * f) *') . k9 = ((x *') * (f *')) . k9 )
assume k9 in dom ((x * f) *') ; :: thesis: ((x * f) *') . k9 = ((x *') * (f *')) . k9
then reconsider k = k9 as Element of NAT ;
(x * f) . k = x * (f . k) by POLYNOM5:def 4;
then ((x * f) *') . k = ((power F_Complex) . ((- (1_ F_Complex)),k)) * ((x * (f . k)) *') by Def9
.= ((power F_Complex) . ((- (1_ F_Complex)),k)) * ((x *') * ((f . k) *')) by COMPLFLD:54
.= (x *') * (((power F_Complex) . ((- (1_ F_Complex)),k)) * ((f . k) *'))
.= (x *') * ((f *') . k) by Def9 ;
hence ((x * f) *') . k9 = ((x *') * (f *')) . k9 by POLYNOM5:def 4; :: thesis: verum

end;

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