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

A1: now

let k9 be set ; :: thesis: ( k9 in dom ((f *') *') implies ((f *') *') . k9 = f . k9 )
assume k9 in dom ((f *') *') ; :: thesis: ((f *') *') . k9 = f . k9
then reconsider k = k9 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:54
.= (((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 *') *') . k9 = f . k9 by VECTSP_1:def 8; :: thesis: verum

end;

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