:: Fundamental Theorem of Algebra
:: by Robert Milewski
::
:: Received August 21, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

theorem Th1: :: POLYNOM5:1
for n, m being Element of NAT st n <> 0 &amp; m <> 0 holds
(((n * m) - n) - m) + 1 >= 0
proofend;

theorem Th2: :: POLYNOM5:2
for x, y being real number st y > 0 holds
(min (x,y)) / (max (x,y)) <= 1
proofend;

theorem Th3: :: POLYNOM5:3
for x, y being real number st ( for c being real number st c > 0 &amp; c < 1 holds
c * x >= y ) holds
y <= 0
proofend;

Lm1:  for x, y being Real st ( for c being Real st c > 0 &amp; c < 1 holds
c * x >= y ) holds
y <= 0
proofend;

theorem Th4: :: POLYNOM5:4
for p being FinSequence of REAL st ( for n being Element of NAT st n in dom p holds
p . n >= 0 ) holds
for i being Element of NAT st i in dom p holds
Sum p >= p . i
proofend;

theorem Th5: :: POLYNOM5:5
for x, y being Real holds - [**x,y**] = [**(- x),(- y)**]
proofend;

theorem Th6: :: POLYNOM5:6
for x1, y1, x2, y2 being Real holds [**x1,y1**] - [**x2,y2**] = [**(x1 - x2),(y1 - y2)**]
proofend;

theorem Th7: :: POLYNOM5:7
for z being Element of F_Complex st z <> 0. F_Complex holds
for n being Element of NAT holds |.((power F_Complex) . (z,n)).| = |.z.| to_power n
proofend;

definition
let p be FinSequence of the carrier of F_Complex;
func|.p.| ->  FinSequence of REAL  means :Def1: :: POLYNOM5:def 1
( len it = len p &amp; ( for n being Element of NAT st n in dom p holds
it /. n = |.(p /. n).| ) );
existence
 ex b1 being FinSequence of REAL st
( len b1 = len p &amp; ( for n being Element of NAT st n in dom p holds
b1 /. n = |.(p /. n).| ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of REAL st len b1 = len p &amp; ( for n being Element of NAT st n in dom p holds
b1 /. n = |.(p /. n).| ) &amp; len b2 = len p &amp; ( for n being Element of NAT st n in dom p holds
b2 /. n = |.(p /. n).| ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines |. POLYNOM5:def_1_:_
 for p being FinSequence of the carrier of F_Complex
for b2 being FinSequence of REAL holds
( b2 = |.p.| iff ( len b2 = len p &amp; ( for n being Element of NAT st n in dom p holds
b2 /. n = |.(p /. n).| ) ) );

theorem Th8: :: POLYNOM5:8
|.(<*> the carrier of F_Complex).| = <*> REAL
proofend;

theorem Th9: :: POLYNOM5:9
for x being Element of F_Complex holds |.<*x*>.| = <*|.x.|*>
proofend;

theorem :: POLYNOM5:10
for x, y being Element of F_Complex holds |.<*x,y*>.| = <*|.x.|,|.y.|*>
proofend;

theorem :: POLYNOM5:11
for x, y, z being Element of F_Complex holds |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*>
proofend;

theorem Th12: :: POLYNOM5:12
for p, q being FinSequence of the carrier of F_Complex holds |.(p ^ q).| = |.p.| ^ |.q.|
proofend;

theorem :: POLYNOM5:13
for p being FinSequence of the carrier of F_Complex
for x being Element of F_Complex holds
( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> &amp; |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )
proofend;

theorem Th14: :: POLYNOM5:14
for p being FinSequence of the carrier of F_Complex holds |.(Sum p).| <= Sum |.p.|
proofend;

begin

definition
let L be non empty right_complementable Abelian add-associative right_zeroed commutative right_unital distributive doubleLoopStr ;
let p be Polynomial of L;
let n be Element of NAT ;
funcp `^ n ->  sequence of L equals :: POLYNOM5:def 2
(power (Polynom-Ring L)) . (p,n);
coherence
 (power (Polynom-Ring L)) . (p,n) is sequence of L
proofend;
end;

:: deftheorem  defines `^ POLYNOM5:def_2_:_
 for L being non empty right_complementable Abelian add-associative right_zeroed commutative right_unital distributive doubleLoopStr
for p being Polynomial of L
for n being Element of NAT holds p `^ n = (power (Polynom-Ring L)) . (p,n);

registration
let L be non empty right_complementable Abelian add-associative right_zeroed commutative right_unital distributive doubleLoopStr ;
let p be Polynomial of L;
let n be Element of NAT ;
clusterp `^ n ->  finite-Support ;
coherence
 p `^ n is finite-Support
proofend;
end;

theorem Th15: :: POLYNOM5:15
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 0 = 1_. L
proofend;

theorem :: POLYNOM5:16
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 1 = p
proofend;

theorem :: POLYNOM5:17
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 2 = p *' p
proofend;

theorem :: POLYNOM5:18
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 3 = (p *' p) *' p
proofend;

theorem Th19: :: POLYNOM5:19
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L
for n being Element of NAT holds p `^ (n + 1) = (p `^ n) *' p
proofend;

theorem Th20: :: POLYNOM5:20
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for n being Element of NAT holds (0_. L) `^ (n + 1) = 0_. L
proofend;

theorem :: POLYNOM5:21
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for n being Element of NAT holds (1_. L) `^ n = 1_. L
proofend;

theorem Th22: :: POLYNOM5:22
for L being Field
for p being Polynomial of L
for x being Element of L
for n being Element of NAT holds eval ((p `^ n),x) = (power L) . ((eval (p,x)),n)
proofend;

Lm2:  for L being non empty ZeroStr
for p being AlgSequence of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L
proofend;

theorem Th23: :: POLYNOM5:23
for L being domRing
for p being Polynomial of L st len p <> 0 holds
for n being Element of NAT holds len (p `^ n) = ((n * (len p)) - n) + 1
proofend;

definition
let L be non empty multMagma ;
let p be sequence of L;
let v be Element of L;
funcv * p ->  sequence of L means :Def3: :: POLYNOM5:def 3
 for n being Element of NAT holds it . n = v * (p . n);
existence
 ex b1 being sequence of L st
for n being Element of NAT holds b1 . n = v * (p . n)
proofend;
uniqueness
 for b1, b2 being sequence of L st ( for n being Element of NAT holds b1 . n = v * (p . n) ) &amp; ( for n being Element of NAT holds b2 . n = v * (p . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines * POLYNOM5:def_3_:_
 for L being non empty multMagma
for p being sequence of L
for v being Element of L
for b4 being sequence of L holds
( b4 = v * p iff for n being Element of NAT holds b4 . n = v * (p . n) );

registration
let L be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let p be Polynomial of L;
let v be Element of L;
clusterv * p ->  finite-Support ;
coherence
 v * p is finite-Support
proofend;
end;

theorem Th24: :: POLYNOM5:24
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for p being Polynomial of L holds len ((0. L) * p) = 0
proofend;

theorem Th25: :: POLYNOM5:25
for L being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for p being Polynomial of L
for v being Element of L st v <> 0. L holds
len (v * p) = len p
proofend;

theorem Th26: :: POLYNOM5:26
for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for p being sequence of L holds (0. L) * p = 0_. L
proofend;

theorem Th27: :: POLYNOM5:27
for L being non empty well-unital multLoopStr
for p being sequence of L holds (1. L) * p = p
proofend;

theorem Th28: :: POLYNOM5:28
for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for v being Element of L holds v * (0_. L) = 0_. L
proofend;

theorem Th29: :: POLYNOM5:29
for L being non empty right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr
for v being Element of L holds v * (1_. L) = <%v%>
proofend;

theorem Th30: :: POLYNOM5:30
for L being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for p being Polynomial of L
for v, x being Element of L holds eval ((v * p),x) = v * (eval (p,x))
proofend;

theorem Th31: :: POLYNOM5:31
for L being non empty right_complementable add-associative right_zeroed unital right-distributive doubleLoopStr
for p being Polynomial of L holds eval (p,(0. L)) = p . 0
proofend;

definition
let L be non empty ZeroStr ;
let z0, z1 be Element of L;
func<%z0,z1%> ->  sequence of L equals :: POLYNOM5:def 4
((0_. L) +* (0,z0)) +* (1,z1);
coherence
 ((0_. L) +* (0,z0)) +* (1,z1) is sequence of L ;
end;

:: deftheorem  defines <% POLYNOM5:def_4_:_
 for L being non empty ZeroStr
for z0, z1 being Element of L holds <%z0,z1%> = ((0_. L) +* (0,z0)) +* (1,z1);

theorem Th32: :: POLYNOM5:32
for L being non empty ZeroStr
for z0 being Element of L holds
( <%z0%> . 0 = z0 &amp; ( for n being Element of NAT st n >= 1 holds
<%z0%> . n = 0. L ) )
proofend;

theorem Th33: :: POLYNOM5:33
for L being non empty ZeroStr
for z0 being Element of L st z0 <> 0. L holds
len <%z0%> = 1
proofend;

theorem Th34: :: POLYNOM5:34
for L being non empty ZeroStr holds <%(0. L)%> = 0_. L
proofend;

theorem Th35: :: POLYNOM5:35
for L being non empty right_complementable add-associative right_zeroed associative commutative well-unital distributive domRing-like doubleLoopStr
for x, y being Element of L holds <%x%> *' <%y%> = <%(x * y)%>
proofend;

theorem Th36: :: POLYNOM5:36
for L being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for n being Element of NAT holds <%x%> `^ n = <%((power L) . (x,n))%>
proofend;

theorem :: POLYNOM5:37
for L being non empty right_complementable add-associative right_zeroed unital doubleLoopStr
for z0, x being Element of L holds eval (<%z0%>,x) = z0
proofend;

theorem Th38: :: POLYNOM5:38
for L being non empty ZeroStr
for z0, z1 being Element of L holds
( <%z0,z1%> . 0 = z0 &amp; <%z0,z1%> . 1 = z1 &amp; ( for n being Nat st n >= 2 holds
<%z0,z1%> . n = 0. L ) )
proofend;

registration
let L be non empty ZeroStr ;
let z0, z1 be Element of L;
cluster<%z0,z1%> ->  finite-Support ;
coherence
 <%z0,z1%> is finite-Support
proofend;
end;

theorem Th39: :: POLYNOM5:39
for L being non empty ZeroStr
for z0, z1 being Element of L holds len <%z0,z1%> <= 2
proofend;

theorem Th40: :: POLYNOM5:40
for L being non empty ZeroStr
for z0, z1 being Element of L st z1 <> 0. L holds
len <%z0,z1%> = 2
proofend;

theorem Th41: :: POLYNOM5:41
for L being non empty ZeroStr
for z0 being Element of L st z0 <> 0. L holds
len <%z0,(0. L)%> = 1
proofend;

theorem Th42: :: POLYNOM5:42
for L being non empty ZeroStr holds <%(0. L),(0. L)%> = 0_. L
proofend;

theorem :: POLYNOM5:43
for L being non empty ZeroStr
for z0 being Element of L holds <%z0,(0. L)%> = <%z0%>
proofend;

theorem Th44: :: POLYNOM5:44
for L being non empty right_complementable add-associative right_zeroed unital left-distributive doubleLoopStr
for z0, z1, x being Element of L holds eval (<%z0,z1%>,x) = z0 + (z1 * x)
proofend;

theorem :: POLYNOM5:45
for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr
for z0, z1, x being Element of L holds eval (<%z0,(0. L)%>,x) = z0
proofend;

theorem :: POLYNOM5:46
for L being non empty right_complementable add-associative right_zeroed unital left-distributive doubleLoopStr
for z0, z1, x being Element of L holds eval (<%(0. L),z1%>,x) = z1 * x
proofend;

theorem Th47: :: POLYNOM5:47
for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr
for z0, z1, x being Element of L holds eval (<%z0,(1. L)%>,x) = z0 + x
proofend;

theorem :: POLYNOM5:48
for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr
for z0, z1, x being Element of L holds eval (<%(0. L),(1. L)%>,x) = x
proofend;

begin

definition
let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ;
let p, q be Polynomial of L;
func Subst (p,q) ->  Polynomial of L means :Def5: :: POLYNOM5:def 5
 ex F being FinSequence of the carrier of (Polynom-Ring L) st
( it = Sum F &amp; len F = len p &amp; ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) );
existence
 ex b1 being Polynomial of L ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b1 = Sum F &amp; len F = len p &amp; ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) )
proofend;
uniqueness
 for b1, b2 being Polynomial of L st ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b1 = Sum F &amp; len F = len p &amp; ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) &amp; ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b2 = Sum F &amp; len F = len p &amp; ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines Subst POLYNOM5:def_5_:_
 for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p, q, b4 being Polynomial of L holds
( b4 = Subst (p,q) iff ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b4 = Sum F &amp; len F = len p &amp; ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) );

theorem Th49: :: POLYNOM5:49
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds Subst ((0_. L),p) = 0_. L
proofend;

theorem :: POLYNOM5:50
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds Subst (p,(0_. L)) = <%(p . 0)%>
proofend;

theorem :: POLYNOM5:51
for L being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for p being Polynomial of L
for x being Element of L holds len (Subst (p,<%x%>)) <= 1
proofend;

theorem Th52: :: POLYNOM5:52
for L being Field
for p, q being Polynomial of L st len p <> 0 &amp; len q > 1 holds
len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
proofend;

theorem Th53: :: POLYNOM5:53
for L being Field
for p, q being Polynomial of L
for x being Element of L holds eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
proofend;

begin

definition
let L be non empty unital doubleLoopStr ;
let p be Polynomial of L;
let x be Element of L;
predx is_a_root_of p means :Def6: :: POLYNOM5:def 6
 eval (p,x) = 0. L;
end;

:: deftheorem Def6 defines is_a_root_of POLYNOM5:def_6_:_
 for L being non empty unital doubleLoopStr
for p being Polynomial of L
for x being Element of L holds
( x is_a_root_of p iff eval (p,x) = 0. L );

definition
let L be non empty unital doubleLoopStr ;
let p be Polynomial of L;
attrp is with_roots  means :Def7: :: POLYNOM5:def 7
 ex x being Element of L st x is_a_root_of p;
end;

:: deftheorem Def7 defines with_roots POLYNOM5:def_7_:_
 for L being non empty unital doubleLoopStr
for p being Polynomial of L holds
( p is with_roots iff ex x being Element of L st x is_a_root_of p );

theorem Th54: :: POLYNOM5:54
for L being non empty unital doubleLoopStr holds 0_. L is with_roots
proofend;

registration
let L be non empty unital doubleLoopStr ;
cluster 0_. L ->  with_roots ;
coherence
 0_. L is with_roots by Th54;
end;

theorem :: POLYNOM5:55
for L being non empty unital doubleLoopStr
for x being Element of L holds x is_a_root_of 0_. L
proofend;

registration
let L be non empty unital doubleLoopStr ;
cluster Relation-like NAT -defined the carrier of L -valued Function-like non empty total quasi_total finite-Support with_roots for Element of K27(K28(NAT, the carrier of L));
existence
 ex b1 being Polynomial of L st b1 is with_roots
proofend;
end;

definition
let L be non empty unital doubleLoopStr ;
attrL is algebraic-closed  means :Def8: :: POLYNOM5:def 8
 for p being Polynomial of L st len p > 1 holds
p is with_roots ;
end;

:: deftheorem Def8 defines algebraic-closed POLYNOM5:def_8_:_
 for L being non empty unital doubleLoopStr holds
( L is algebraic-closed iff for p being Polynomial of L st len p > 1 holds
p is with_roots );

definition
let L be non empty unital doubleLoopStr ;
let p be Polynomial of L;
func Roots p ->  Subset of L means :Def9: :: POLYNOM5:def 9
 for x being Element of L holds
( x in it iff x is_a_root_of p );
existence
 ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is_a_root_of p )
proofend;
uniqueness
 for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is_a_root_of p ) ) &amp; ( for x being Element of L holds
( x in b2 iff x is_a_root_of p ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines Roots POLYNOM5:def_9_:_
 for L being non empty unital doubleLoopStr
for p being Polynomial of L
for b3 being Subset of L holds
( b3 = Roots p iff for x being Element of L holds
( x in b3 iff x is_a_root_of p ) );

definition
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;
let p be Polynomial of L;
func NormPolynomial p ->  sequence of L means :Def10: :: POLYNOM5:def 10
 for n being Element of NAT holds it . n = (p . n) / (p . ((len p) -' 1));
existence
 ex b1 being sequence of L st
for n being Element of NAT holds b1 . n = (p . n) / (p . ((len p) -' 1))
proofend;
uniqueness
 for b1, b2 being sequence of L st ( for n being Element of NAT holds b1 . n = (p . n) / (p . ((len p) -' 1)) ) &amp; ( for n being Element of NAT holds b2 . n = (p . n) / (p . ((len p) -' 1)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines NormPolynomial POLYNOM5:def_10_:_
 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for p being Polynomial of L
for b3 being sequence of L holds
( b3 = NormPolynomial p iff for n being Element of NAT holds b3 . n = (p . n) / (p . ((len p) -' 1)) );

registration
let L be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
let p be Polynomial of L;
cluster NormPolynomial p ->  finite-Support ;
coherence
 NormPolynomial p is finite-Support
proofend;
end;

theorem Th56: :: POLYNOM5:56
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for p being Polynomial of L st len p <> 0 holds
(NormPolynomial p) . ((len p) -' 1) = 1. L
proofend;

theorem Th57: :: POLYNOM5:57
for L being Field
for p being Polynomial of L st len p <> 0 holds
len (NormPolynomial p) = len p
proofend;

theorem Th58: :: POLYNOM5:58
for L being Field
for p being Polynomial of L st len p <> 0 holds
for x being Element of L holds eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1))
proofend;

theorem Th59: :: POLYNOM5:59
for L being Field
for p being Polynomial of L st len p <> 0 holds
for x being Element of L holds
( x is_a_root_of p iff x is_a_root_of NormPolynomial p )
proofend;

theorem Th60: :: POLYNOM5:60
for L being Field
for p being Polynomial of L st len p <> 0 holds
( p is with_roots iff NormPolynomial p is with_roots )
proofend;

theorem :: POLYNOM5:61
for L being Field
for p being Polynomial of L st len p <> 0 holds
Roots p = Roots (NormPolynomial p)
proofend;

theorem Th62: :: POLYNOM5:62
id COMPLEX is_continuous_on COMPLEX
proofend;

theorem Th63: :: POLYNOM5:63
for x being Element of COMPLEX holds COMPLEX --> x is_continuous_on COMPLEX
proofend;

definition
let L be non empty unital multMagma ;
let x be Element of L;
let n be Element of NAT ;
func FPower (x,n) ->  Function of L,L means :Def11: :: POLYNOM5:def 11
 for y being Element of L holds it . y = x * ((power L) . (y,n));
existence
 ex b1 being Function of L,L st
for y being Element of L holds b1 . y = x * ((power L) . (y,n))
proofend;
uniqueness
 for b1, b2 being Function of L,L st ( for y being Element of L holds b1 . y = x * ((power L) . (y,n)) ) &amp; ( for y being Element of L holds b2 . y = x * ((power L) . (y,n)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines FPower POLYNOM5:def_11_:_
 for L being non empty unital multMagma
for x being Element of L
for n being Element of NAT
for b4 being Function of L,L holds
( b4 = FPower (x,n) iff for y being Element of L holds b4 . y = x * ((power L) . (y,n)) );

theorem :: POLYNOM5:64
for L being non empty unital multMagma holds FPower ((1_ L),1) = id the carrier of L
proofend;

theorem :: POLYNOM5:65
FPower ((1_ F_Complex),2) = (id COMPLEX) (#) (id COMPLEX)
proofend;

theorem Th66: :: POLYNOM5:66
for L being non empty unital multMagma
for x being Element of L holds FPower (x,0) = the carrier of L --> x
proofend;

theorem :: POLYNOM5:67
for x being Element of F_Complex ex x1 being Element of COMPLEX st
( x = x1 &amp; FPower (x,1) = x1 (#) (id COMPLEX) )
proofend;

theorem :: POLYNOM5:68
for x being Element of F_Complex ex x1 being Element of COMPLEX st
( x = x1 &amp; FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) )
proofend;

theorem Th69: :: POLYNOM5:69
for x being Element of F_Complex
for n being Element of NAT ex f being Function of COMPLEX,COMPLEX st
( f = FPower (x,n) &amp; FPower (x,(n + 1)) = f (#) (id COMPLEX) )
proofend;

theorem Th70: :: POLYNOM5:70
for x being Element of F_Complex
for n being Element of NAT ex f being Function of COMPLEX,COMPLEX st
( f = FPower (x,n) &amp; f is_continuous_on COMPLEX )
proofend;

definition
let L be non empty well-unital doubleLoopStr ;
let p be Polynomial of L;
func Polynomial-Function (L,p) ->  Function of L,L means :Def12: :: POLYNOM5:def 12
 for x being Element of L holds it . x = eval (p,x);
existence
 ex b1 being Function of L,L st
for x being Element of L holds b1 . x = eval (p,x)
proofend;
uniqueness
 for b1, b2 being Function of L,L st ( for x being Element of L holds b1 . x = eval (p,x) ) &amp; ( for x being Element of L holds b2 . x = eval (p,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines Polynomial-Function POLYNOM5:def_12_:_
 for L being non empty well-unital doubleLoopStr
for p being Polynomial of L
for b3 being Function of L,L holds
( b3 = Polynomial-Function (L,p) iff for x being Element of L holds b3 . x = eval (p,x) );

theorem Th71: :: POLYNOM5:71
for p being Polynomial of F_Complex ex f being Function of COMPLEX,COMPLEX st
( f = Polynomial-Function (F_Complex,p) &amp; f is_continuous_on COMPLEX )
proofend;

theorem Th72: :: POLYNOM5:72
for p being Polynomial of F_Complex st len p > 2 &amp; |.(p . ((len p) -' 1)).| = 1 holds
for F being FinSequence of REAL st len F = len p &amp; ( for n being Element of NAT st n in dom F holds
F . n = |.(p . (n -' 1)).| ) holds
for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval (p,z)).| > |.(p . 0).| + 1
proofend;

theorem Th73: :: POLYNOM5:73
for p being Polynomial of F_Complex st len p > 2 holds
ex z0 being Element of F_Complex st
for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).|
proofend;

:: [WP: ] Fundamental_Theorem_of_Algebra
theorem Th74: :: POLYNOM5:74
for p being Polynomial of F_Complex st len p > 1 holds
p is with_roots
proofend;

registration
cluster F_Complex  ->  algebraic-closed ;
coherence
 F_Complex is algebraic-closed by Def8, Th74;
end;

registration
cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right_unital well-unital distributive left_unital algebraic-closed for doubleLoopStr ;
existence
 ex b1 being non empty well-unital doubleLoopStr st
( b1 is algebraic-closed &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is Abelian &amp; b1 is commutative &amp; b1 is associative &amp; b1 is distributive &amp; b1 is almost_left_invertible &amp; not b1 is degenerated )
proofend;
end;