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: dom ((x * f) *' ) = NAT by FUNCT_2:def 1
.= dom ((x *' ) * (f *' )) by FUNCT_2:def 1 ;

now

let k' be set ; :: thesis: ( k' in dom ((x * f) *' ) implies ((x * f) *' ) . k' = ((x *' ) * (f *' )) . k' )
assume k' in dom ((x * f) *' ) ; :: thesis: ((x * f) *' ) . k' = ((x *' ) * (f *' )) . k'
then reconsider k = k' as Element of NAT ;
(x * f) . k = x * (f . k) by POLYNOM5:def 3;
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:90
.= (x *' ) * (((power F_Complex ) . (- (1_ F_Complex )),k) * ((f . k) *' ))
.= (x *' ) * ((f *' ) . k) by Def9 ;
hence ((x * f) *' ) . k' = ((x *' ) * (f *' )) . k' by POLYNOM5:def 3; :: thesis: verum

end;

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