let c be Element of F_Complex; :: thesis:
thus ( ex f being INT -valued non-zero Polynomial of F_Complex st c is_a_root_of f implies ex f being RAT -valued monic Polynomial of F_Complex st c is_a_root_of f ) :: thesis:

given f being INT -valued non-zero Polynomial of F_Complex such that A1: c is_a_root_of f ; :: thesis:
f <> 0_. F_Complex ;
then A2: len f <> 0 by POLYNOM4:5;
rng (NormPolynomial f) c= RAT

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in rng (NormPolynomial f) ; :: thesis:
then consider x being object such that
A3: ( x in dom (NormPolynomial f) & o = (NormPolynomial f) . x ) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A3;
reconsider fix = f . x, fil = f . ((len f) -' 1) as Integer ;
A4: f . ((len f) -' 1) = LC f ;
o = (f . x) / (f . ((len f) -' 1)) by A3, POLYNOM5:def 11
.= fix / fil by A4, COMPLFLD:6 ;
hence o in RAT by RAT_1:def 1; :: thesis:

end;

then reconsider g = NormPolynomial f as RAT -valued monic Polynomial of F_Complex by RELAT_1:def 19;
take g ; :: thesis:
thus c is_a_root_of g by A1, A2, POLYNOM5:59; :: thesis:

end;

given f being RAT -valued monic Polynomial of F_Complex such that A5: c is_a_root_of f ; :: thesis:
f <> 0_. F_Complex ;
then A6: len f <> 0 by POLYNOM4:5;
reconsider lf = len f as Element of NAT ;
deffunc H₁( Element of NAT ) -> Element of the carrier of F_Complex = In ((denominator (f . $1)),F_Complex);
consider d being Polynomial of F_Complex such that
A7: ( len d <= lf & ( for n being Element of NAT st n < lf holds
d . n = H₁(n) ) ) from POLYNOM3:sch 2();

assume A8: len d < lf ; :: thesis:
then reconsider lf1 = lf - 1 as Element of NAT by NAT_1:20;
len d < lf1 + 1 by A8;
then A9: len d <= lf1 by NAT_1:13;
d . lf1 = H₁(lf1) by A7, XREAL_1:44;
then d . lf1 <> 0. F_Complex by COMPLFLD:def 1;
hence contradiction by A9, ALGSEQ_1:8; :: thesis:

end;

then A10: len d = len f by A7, XXREAL_0:1;
deffunc H₂( Nat) -> Element of the carrier of F_Complex = d . ($1 -' 1);
consider df being FinSequence such that
A11: ( len df = len d & ( for k being Nat st k in dom df holds
df . k = H₂(k) ) ) from FINSEQ_1:sch 2();
A12: rng df c= INT

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in rng df ; :: thesis:
then consider a being object such that
A13: ( a in dom df & o = df . a ) by FUNCT_1:def 3;
reconsider a = a as Element of NAT by A13;
A14: ( 1 <= a & a <= len df ) by A13, FINSEQ_3:25;
then a -' 1 = a - 1 by XREAL_0:def 2;
then A15: a -' 1 < len f by A10, A11, A14, XREAL_1:231;
df . a = d . (a -' 1) by A13, A11
.= In ((denominator (f . (a -' 1))),F_Complex) by A15, A7
.= denominator (f . (a -' 1)) ;
hence o in INT by A13, INT_1:def 2; :: thesis:

end;

then reconsider df = df as INT -valued FinSequence by RELAT_1:def 19;
rng df c= COMPLEX by A12, NUMBERS:16;
then rng df c= the carrier of F_Complex by COMPLFLD:def 1;
then reconsider dfc = df as FinSequence of F_Complex by FINSEQ_1:def 4;
Product df in COMPLEX by XCMPLX_0:def 2;
then reconsider dd = Product df as Element of F_Complex by COMPLFLD:def 1;
A16: for i being Nat st i in dom dfc holds
dfc . i <> 0. F_Complex

let i be Nat; :: thesis:
assume A17: i in dom dfc ; :: thesis:
then reconsider a = i as Element of NAT ;
A18: ( 1 <= a & a <= len df ) by A17, FINSEQ_3:25;
then a -' 1 = a - 1 by XREAL_0:def 2;
then A19: a -' 1 < len f by A10, A11, A18, XREAL_1:231;
df . a = d . (a -' 1) by A17, A11
.= In ((denominator (f . (a -' 1))),F_Complex) by A19, A7
.= denominator (f . (a -' 1)) ;
hence dfc . i <> 0. F_Complex by COMPLFLD:def 1; :: thesis:

end;

A20: ( the multF of F_Complex = multcomplex & the carrier of F_Complex = COMPLEX ) by COMPLFLD:def 1;
consider dfo being FinSequence of COMPLEX such that
A21: ( dfo = df & Product df = multcomplex $$ dfo ) by RVSUM_1:def 13;
Product df = Product dfc by A20, A21, GROUP_4:def 2;
then A22: len (dd * f) > 0 by A16, A6, POLYNOM5:25, RING_2:2;
rng (dd * f) c= INT

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in rng (dd * f) ; :: thesis:
then consider a being object such that
A23: ( a in dom (dd * f) & o = (dd * f) . a ) by FUNCT_1:def 3;
reconsider a = a as Element of NAT by A23;
A24: o = dd * (f . a) by A23, POLYNOM5:def 4
.= (Product df) * (f . a) ;

suppose a >= len f ; :: thesis:

then f . a = 0. F_Complex by ALGSEQ_1:8;
then o = (Product df) * 0 by A24, COMPLFLD:def 1
.= 0 ;
hence o in INT by INT_1:def 2; :: thesis:

end;

suppose A25: a < len f ; :: thesis:

then A26: ( 1 <= a + 1 & a + 1 <= len df ) by A11, A10, NAT_1:12, NAT_1:13;
then A27: a + 1 in dom df by FINSEQ_3:25;
df . (a + 1) = d . ((a + 1) -' 1) by A11, A26, FINSEQ_3:25
.= d . a by NAT_D:34
.= In ((denominator (f . a)),F_Complex) by A25, A7
.= denominator (f . a) ;
then denominator (f . a) in rng df by A27, FUNCT_1:def 3;
then denominator (f . a) divides Product df by Th23;
then consider j being Integer such that
A28: Product df = (denominator (f . a)) * j ;
f . a = (numerator (f . a)) / (denominator (f . a)) by RAT_1:15;
then o = j * (numerator (f . a)) by A28, A24, XCMPLX_1:90;
hence o in INT by INT_1:def 2; :: thesis:

end;

end;

end;

then reconsider g = dd * f as INT -valued non-zero Polynomial of F_Complex by RELAT_1:def 19, UPROOTS:17, A22;
take g ; :: thesis:
eval (g,c) = dd * (0. F_Complex) by A5, POLYNOM5:30;
hence c is_a_root_of g ; :: thesis: