let g, f be Polynomial of F_Complex; :: thesis: ( ( for i being Element of NAT holds g . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) implies for i being Element of NAT holds f . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((g . i) *') )
assume A7: for i being Element of NAT holds g . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ; :: thesis: for i being Element of NAT holds f . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((g . i) *')
let i be Element of NAT ; :: thesis: f . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((g . i) *')
thus f . i = (1_ F_Complex) * (f . i)
.= ((power F_Complex) . ((- (1_ F_Complex)),(2 * i))) * (f . i) by Th4
.= ((power F_Complex) . ((- (1_ F_Complex)),(i + i))) * (f . i)
.= (((power F_Complex) . ((- (1_ F_Complex)),i)) * ((power F_Complex) . ((- (1_ F_Complex)),i))) * (f . i) by Th3
.= (((power F_Complex) . ((- (1_ F_Complex)),i)) * ((power F_Complex) . (((- (1_ F_Complex)) *'),i))) * (f . i) by Lm2, COMPLEX1:38
.= (((power F_Complex) . ((- (1_ F_Complex)),i)) * (((power F_Complex) . ((- (1_ F_Complex)),i)) *')) * (f . i) by Th5
.= ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((((power F_Complex) . ((- (1_ F_Complex)),i)) *') * (((f . i) *') *'))
.= ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *')) *') by COMPLFLD:54
.= ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((g . i) *') by A7 ; :: thesis: verum