let f be Polynomial of F_Complex ; :: thesis: (f *' ) *' = f
set g = (f *' ) *' ;
A1: dom ((f *' ) *' ) = NAT by FUNCT_2:def 1
.= dom f by FUNCT_2:def 1 ;

now

let k' be set ; :: thesis: ( k' in dom ((f *' ) *' ) implies ((f *' ) *' ) . k' = f . k' )
assume k' in dom ((f *' ) *' ) ; :: thesis: ((f *' ) *' ) . k' = f . k'
then reconsider k = k' as Element of NAT ;
((f *' ) *' ) . k = ((power F_Complex ) . (- (1_ F_Complex )),k) * (((f *' ) . k) *' ) by Def9
.= ((power F_Complex ) . (- (1_ F_Complex )),k) * ((((power F_Complex ) . (- (1_ F_Complex )),k) * ((f . k) *' )) *' ) by Def9
.= ((power F_Complex ) . (- (1_ F_Complex )),k) * ((((power F_Complex ) . (- (1_ F_Complex )),k) *' ) * (((f . k) *' ) *' )) by COMPLFLD:90
.= (((power F_Complex ) . (- (1_ F_Complex )),k) * (((power F_Complex ) . (- (1_ F_Complex )),k) *' )) * (f . k)
.= (((power F_Complex ) . (- (1_ F_Complex )),k) * ((power F_Complex ) . ((- (1_ F_Complex )) *' ),k)) * (f . k) by Th5
.= (((power F_Complex ) . (- (1_ F_Complex )),k) * ((power F_Complex ) . (- (1_ F_Complex )),k)) * (f . k) by Lm2, Lm3
.= ((power F_Complex ) . (- (1_ F_Complex )),(k + k)) * (f . k) by Th3
.= ((power F_Complex ) . (- (1_ F_Complex )),(2 * k)) * (f . k)
.= (1_ F_Complex ) * (f . k) by Th4 ;
hence ((f *' ) *' ) . k' = f . k' by VECTSP_1:def 19; :: thesis: verum

end;

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