:: POLYNOM5 semantic presentation

theorem Th1: :: POLYNOM5:1

for b₁, b₂ being Nat st b₁ <> 0 & b₂ <> 0 holds
(((b₁ * b₂) - b₁) - b₂) + 1 >= 0

proof end;

theorem Th2: :: POLYNOM5:2

for b₁, b₂ being real number st b₂ > 0 holds
(min b₁,b₂) / (max b₁,b₂) <= 1

proof end;

theorem Th3: :: POLYNOM5:3

for b₁, b₂ being real number st ( for b₃ being real number st b₃ > 0 & b₃ < 1 holds
b₃ * b₁ >= b₂ ) holds
b₂ <= 0

proof end;

Lemma4: for b₁, b₂ being Real st ( for b₃ being Real st b₃ > 0 & b₃ < 1 holds
b₃ * b₁ >= b₂ ) holds
b₂ <= 0

proof end;

theorem Th4: :: POLYNOM5:4

for b₁ being FinSequence of REAL st ( for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ >= 0 ) holds
for b₂ being Nat st b₂ in dom b₁ holds
Sum b₁ >= b₁ . b₂

proof end;

theorem Th5: :: POLYNOM5:5

for b₁, b₂ being Real holds - [**b₁,b₂**] = [**(- b₁),(- b₂)**]

proof end;

theorem Th6: :: POLYNOM5:6

for b₁, b₂, b₃, b₄ being Real holds [**b₁,b₂**] - [**b₃,b₄**] = [**(b₁ - b₃),(b₂ - b₄)**]

proof end;

theorem Th7: :: POLYNOM5:7

canceled;

theorem Th8: :: POLYNOM5:8

for b₁ being Element of F_Complex st b₁ <> 0. F_Complex holds
for b₂ being Nat holds |.((power F_Complex ) . b₁,b₂).| = |.b₁.| to_power b₂

proof end;

definition

let c₁ be FinSequence of the carrier of F_Complex ;
func |.c₁.| -> FinSequence of REAL means :Def1: :: POLYNOM5:def 1
( len a₂ = len a₁ & ( for b₁ being Nat st b₁ in dom a₁ holds
a₂ /. b₁ = |.(a₁ /. b₁).| ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines |. POLYNOM5:def 1 :

theorem Th9: :: POLYNOM5:9

|.(<*> the carrier of F_Complex ).| = <*> REAL

proof end;

theorem Th10: :: POLYNOM5:10

for b₁ being Element of F_Complex holds |.<*b₁*>.| = <*|.b₁.|*>

proof end;

theorem Th11: :: POLYNOM5:11

for b₁, b₂ being Element of F_Complex holds |.<*b₁,b₂*>.| = <*|.b₁.|,|.b₂.|*>

proof end;

theorem Th12: :: POLYNOM5:12

for b₁, b₂, b₃ being Element of F_Complex holds |.<*b₁,b₂,b₃*>.| = <*|.b₁.|,|.b₂.|,|.b₃.|*>

proof end;

theorem Th13: :: POLYNOM5:13

for b₁, b₂ being FinSequence of the carrier of F_Complex holds |.(b₁ ^ b₂).| = |.b₁.| ^ |.b₂.|

proof end;

theorem Th14: :: POLYNOM5:14

for b₁ being FinSequence of the carrier of F_Complex
for b₂ being Element of F_Complex holds
( |.(b₁ ^ <*b₂*>).| = |.b₁.| ^ <*|.b₂.|*> & |.(<*b₂*> ^ b₁).| = <*|.b₂.|*> ^ |.b₁.| )

proof end;

theorem Th15: :: POLYNOM5:15

for b₁ being FinSequence of the carrier of F_Complex holds |.(Sum b₁).| <= Sum |.b₁.|

proof end;

definition

let c₁ be non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr ;
let c₂ be Polynomial of c₁;
let c₃ be Nat;
func c₂ `^ c₃ -> sequence of a₁ equals :: POLYNOM5:def 2
(power (Polynom-Ring a₁)) . a₂,a₃;
coherence

proof end;

end;

:: deftheorem Def2 defines `^ POLYNOM5:def 2 :

registration

let c₁ be non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr ;
let c₂ be Polynomial of c₁;
let c₃ be Nat;
cluster a₂ `^ a₃ -> finite-Support ;
coherence

proof end;

end;

theorem Th16: :: POLYNOM5:16

for b₁ being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for b₂ being Polynomial of b₁ holds b₂ `^ 0 = 1_. b₁

proof end;

theorem Th17: :: POLYNOM5:17

for b₁ being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for b₂ being Polynomial of b₁ holds b₂ `^ 1 = b₂

proof end;

theorem Th18: :: POLYNOM5:18

for b₁ being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for b₂ being Polynomial of b₁ holds b₂ `^ 2 = b₂ *' b₂

proof end;

theorem Th19: :: POLYNOM5:19

for b₁ being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for b₂ being Polynomial of b₁ holds b₂ `^ 3 = (b₂ *' b₂) *' b₂

proof end;

theorem Th20: :: POLYNOM5:20

for b₁ being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for b₂ being Polynomial of b₁
for b₃ being Nat holds b₂ `^ (b₃ + 1) = (b₂ `^ b₃) *' b₂

proof end;

theorem Th21: :: POLYNOM5:21

for b₁ being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for b₂ being Nat holds (0_. b₁) `^ (b₂ + 1) = 0_. b₁

proof end;

theorem Th22: :: POLYNOM5:22

for b₁ being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for b₂ being Nat holds (1_. b₁) `^ b₂ = 1_. b₁

proof end;

theorem Th23: :: POLYNOM5:23

for b₁ being Field
for b₂ being Polynomial of b₁
for b₃ being Element of b₁
for b₄ being Nat holds eval (b₂ `^ b₄),b₃ = (power b₁) . (eval b₂,b₃),b₄

proof end;

Lemma18: for b₁ being non empty ZeroStr
for b₂ being AlgSequence of b₁ st len b₂ > 0 holds
b₂ . ((len b₂) -' 1) <> 0. b₁

proof end;

theorem Th24: :: POLYNOM5:24

for b₁ being domRing
for b₂ being Polynomial of b₁ st len b₂ <> 0 holds
for b₃ being Nat holds len (b₂ `^ b₃) = ((b₃ * (len b₂)) - b₃) + 1

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂ be sequence of c₁;
let c₃ be Element of c₁;
func c₃ * c₂ -> sequence of a₁ means :Def3: :: POLYNOM5:def 3
for b₁ being Nat holds a₄ . b₁ = a₃ * (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines * POLYNOM5:def 3 :

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be Polynomial of c₁;
let c₃ be Element of c₁;
cluster a₃ * a₂ -> finite-Support ;
coherence

proof end;

end;

theorem Th25: :: POLYNOM5:25

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being Polynomial of b₁ holds len ((0. b₁) * b₂) = 0

proof end;

theorem Th26: :: POLYNOM5:26

for b₁ being non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital Field-like doubleLoopStr
for b₂ being Polynomial of b₁
for b₃ being Element of b₁ st b₃ <> 0. b₁ holds
len (b₃ * b₂) = len b₂

proof end;

theorem Th27: :: POLYNOM5:27

for b₁ being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂ being sequence of b₁ holds (0. b₁) * b₂ = 0_. b₁

proof end;

theorem Th28: :: POLYNOM5:28

for b₁ being non empty left_unital multLoopStr
for b₂ being sequence of b₁ holds (1. b₁) * b₂ = b₂

proof end;

theorem Th29: :: POLYNOM5:29

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂ being Element of b₁ holds b₂ * (0_. b₁) = 0_. b₁

proof end;

theorem Th30: :: POLYNOM5:30

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive right_unital doubleLoopStr
for b₂ being Element of b₁ holds b₂ * (1_. b₁) = <%b₂%>

proof end;

theorem Th31: :: POLYNOM5:31

for b₁ being non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital Field-like doubleLoopStr
for b₂ being Polynomial of b₁
for b₃, b₄ being Element of b₁ holds eval (b₃ * b₂),b₄ = b₃ * (eval b₂,b₄)

proof end;

theorem Th32: :: POLYNOM5:32

for b₁ being non empty unital add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂ being Polynomial of b₁ holds eval b₂,(0. b₁) = b₂ . 0

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂, c₃ be Element of c₁;
func <%c₂,c₃%> -> sequence of a₁ equals :: POLYNOM5:def 4
((0_. a₁) +* 0,a₂) +* 1,a₃;
coherence ;

end;

:: deftheorem Def4 defines <% POLYNOM5:def 4 :

theorem Th33: :: POLYNOM5:33

for b₁ being non empty ZeroStr
for b₂ being Element of b₁ holds
( <%b₂%> . 0 = b₂ & ( for b₃ being Nat st b₃ >= 1 holds
<%b₂%> . b₃ = 0. b₁ ) )

proof end;

theorem Th34: :: POLYNOM5:34

for b₁ being non empty ZeroStr
for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
len <%b₂%> = 1

proof end;

theorem Th35: :: POLYNOM5:35

for b₁ being non empty ZeroStr holds <%(0. b₁)%> = 0_. b₁

proof end;

theorem Th36: :: POLYNOM5:36

for b₁ being non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital domRing-like doubleLoopStr
for b₂, b₃ being Element of b₁ holds <%b₂%> *' <%b₃%> = <%(b₂ * b₃)%>

proof end;

theorem Th37: :: POLYNOM5:37

for b₁ being non empty associative commutative Abelian add-associative right_zeroed right_complementable right_unital distributive Field-like doubleLoopStr
for b₂ being Element of b₁
for b₃ being Nat holds <%b₂%> `^ b₃ = <%((power b₁) . b₂,b₃)%>

proof end;

theorem Th38: :: POLYNOM5:38

for b₁ being non empty unital add-associative right_zeroed right_complementable doubleLoopStr
for b₂, b₃ being Element of b₁ holds eval <%b₂%>,b₃ = b₂

proof end;

theorem Th39: :: POLYNOM5:39

for b₁ being non empty ZeroStr
for b₂, b₃ being Element of b₁ holds
( <%b₂,b₃%> . 0 = b₂ & <%b₂,b₃%> . 1 = b₃ & ( for b₄ being Nat st b₄ >= 2 holds
<%b₂,b₃%> . b₄ = 0. b₁ ) )

proof end;

registration

let c₁ be non empty ZeroStr ;
let c₂, c₃ be Element of c₁;
cluster <%a₂,a₃%> -> finite-Support ;
coherence

proof end;

end;

theorem Th40: :: POLYNOM5:40

for b₁ being non empty ZeroStr
for b₂, b₃ being Element of b₁ holds len <%b₂,b₃%> <= 2

proof end;

theorem Th41: :: POLYNOM5:41

for b₁ being non empty ZeroStr
for b₂, b₃ being Element of b₁ st b₃ <> 0. b₁ holds
len <%b₂,b₃%> = 2

proof end;

theorem Th42: :: POLYNOM5:42

for b₁ being non empty ZeroStr
for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
len <%b₂,(0. b₁)%> = 1

proof end;

theorem Th43: :: POLYNOM5:43

for b₁ being non empty ZeroStr holds <%(0. b₁),(0. b₁)%> = 0_. b₁

proof end;

theorem Th44: :: POLYNOM5:44

for b₁ being non empty ZeroStr
for b₂ being Element of b₁ holds <%b₂,(0. b₁)%> = <%b₂%>

proof end;

theorem Th45: :: POLYNOM5:45

for b₁ being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂, b₃, b₄ being Element of b₁ holds eval <%b₂,b₃%>,b₄ = b₂ + (b₃ * b₄)

proof end;

theorem Th46: :: POLYNOM5:46

for b₁ being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂, b₃, b₄ being Element of b₁ holds eval <%b₂,(0. b₁)%>,b₄ = b₂

proof end;

theorem Th47: :: POLYNOM5:47

for b₁ being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂, b₃, b₄ being Element of b₁ holds eval <%(0. b₁),b₃%>,b₄ = b₃ * b₄

proof end;

theorem Th48: :: POLYNOM5:48

for b₁ being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂, b₃, b₄ being Element of b₁ holds eval <%b₂,(1. b₁)%>,b₄ = b₂ + b₄

proof end;

theorem Th49: :: POLYNOM5:49

for b₁ being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂, b₃, b₄ being Element of b₁ holds eval <%(0. b₁),(1. b₁)%>,b₄ = b₄

proof end;

definition

let c₁ be non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr ;
let c₂, c₃ be Polynomial of c₁;
func Subst c₂,c₃ -> Polynomial of a₁ means :Def5: :: POLYNOM5:def 5
ex b₁ being FinSequence of the carrier of (Polynom-Ring a₁) st
( a₄ = Sum b₁ & len b₁ = len a₂ & ( for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ = (a₂ . (b₂ -' 1)) * (a₃ `^ (b₂ -' 1)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Subst POLYNOM5:def 5 :

theorem Th50: :: POLYNOM5:50

for b₁ being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for b₂ being Polynomial of b₁ holds Subst (0_. b₁),b₂ = 0_. b₁

proof end;

theorem Th51: :: POLYNOM5:51

proof end;

theorem Th52: :: POLYNOM5:52

for b₁ being non empty associative commutative Abelian add-associative right_zeroed right_complementable right_unital distributive Field-like doubleLoopStr
for b₂ being Polynomial of b₁
for b₃ being Element of b₁ holds len (Subst b₂,<%b₃%>) <= 1

proof end;

theorem Th53: :: POLYNOM5:53

for b₁ being Field
for b₂, b₃ being Polynomial of b₁ st len b₂ <> 0 & len b₃ > 1 holds
len (Subst b₂,b₃) = ((((len b₂) * (len b₃)) - (len b₂)) - (len b₃)) + 2

proof end;

theorem Th54: :: POLYNOM5:54

for b₁ being Field
for b₂, b₃ being Polynomial of b₁
for b₄ being Element of b₁ holds eval (Subst b₂,b₃),b₄ = eval b₂,(eval b₃,b₄)

proof end;

definition

let c₁ be non empty unital doubleLoopStr ;
let c₂ be Polynomial of c₁;
let c₃ be Element of c₁;
pred c₃ is_a_root_of c₂ means :Def6: :: POLYNOM5:def 6
eval a₂,a₃ = 0. a₁;

end;

:: deftheorem Def6 defines is_a_root_of POLYNOM5:def 6 :

definition

let c₁ be non empty unital doubleLoopStr ;
let c₂ be Polynomial of c₁;
attr a₂ is with_roots means :Def7: :: POLYNOM5:def 7
ex b₁ being Element of a₁ st b₁ is_a_root_of a₂;

end;

:: deftheorem Def7 defines with_roots POLYNOM5:def 7 :

theorem Th55: :: POLYNOM5:55

for b₁ being non empty unital doubleLoopStr holds 0_. b₁ is with_roots

proof end;

registration

let c₁ be non empty unital doubleLoopStr ;
cluster 0_. a₁ -> with_roots ;
coherence by Th55;

end;

theorem Th56: :: POLYNOM5:56

for b₁ being non empty unital doubleLoopStr
for b₂ being Element of b₁ holds b₂ is_a_root_of 0_. b₁

proof end;

registration

let c₁ be non empty unital doubleLoopStr ;
cluster with_roots M5( NAT ,the carrier of a₁);
existence

proof end;

end;

definition

let c₁ be non empty unital doubleLoopStr ;
attr a₁ is algebraic-closed means :Def8: :: POLYNOM5:def 8
for b₁ being Polynomial of a₁ st len b₁ > 1 holds
b₁ is with_roots;

end;

:: deftheorem Def8 defines algebraic-closed POLYNOM5:def 8 :

definition

let c₁ be non empty unital doubleLoopStr ;
let c₂ be Polynomial of c₁;
func Roots c₂ -> Subset of a₁ means :Def9: :: POLYNOM5:def 9
for b₁ being Element of a₁ holds
( b₁ in a₃ iff b₁ is_a_root_of a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Roots POLYNOM5:def 9 :

definition

let c₁ be non empty associative commutative distributive left_unital Field-like doubleLoopStr ;
let c₂ be Polynomial of c₁;
func NormPolynomial c₂ -> sequence of a₁ means :Def10: :: POLYNOM5:def 10
for b₁ being Nat holds a₃ . b₁ = (a₂ . b₁) / (a₂ . ((len a₂) -' 1));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines NormPolynomial POLYNOM5:def 10 :

registration

let c₁ be non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital Field-like doubleLoopStr ;
let c₂ be Polynomial of c₁;
cluster NormPolynomial a₂ -> finite-Support ;
coherence

proof end;

end;

theorem Th57: :: POLYNOM5:57

for b₁ being non empty associative commutative distributive left_unital Field-like doubleLoopStr
for b₂ being Polynomial of b₁ st len b₂ <> 0 holds
(NormPolynomial b₂) . ((len b₂) -' 1) = 1. b₁

proof end;

theorem Th58: :: POLYNOM5:58

for b₁ being Field
for b₂ being Polynomial of b₁ st len b₂ <> 0 holds
len (NormPolynomial b₂) = len b₂

proof end;

theorem Th59: :: POLYNOM5:59

for b₁ being Field
for b₂ being Polynomial of b₁ st len b₂ <> 0 holds
for b₃ being Element of b₁ holds eval (NormPolynomial b₂),b₃ = (eval b₂,b₃) / (b₂ . ((len b₂) -' 1))

proof end;

theorem Th60: :: POLYNOM5:60

for b₁ being Field
for b₂ being Polynomial of b₁ st len b₂ <> 0 holds
for b₃ being Element of b₁ holds
( b₃ is_a_root_of b₂ iff b₃ is_a_root_of NormPolynomial b₂ )

proof end;

theorem Th61: :: POLYNOM5:61

for b₁ being Field
for b₂ being Polynomial of b₁ st len b₂ <> 0 holds
( b₂ is with_roots iff NormPolynomial b₂ is with_roots )

proof end;

theorem Th62: :: POLYNOM5:62

for b₁ being Field
for b₂ being Polynomial of b₁ st len b₂ <> 0 holds
Roots b₂ = Roots (NormPolynomial b₂)

proof end;

theorem Th63: :: POLYNOM5:63

id COMPLEX is_continuous_on COMPLEX

proof end;

theorem Th64: :: POLYNOM5:64

for b₁ being Element of COMPLEX holds COMPLEX --> b₁ is_continuous_on COMPLEX

proof end;

definition

let c₁ be non empty unital HGrStr ;
let c₂ be Element of c₁;
let c₃ be Nat;
func FPower c₂,c₃ -> Function of a₁,a₁ means :Def11: :: POLYNOM5:def 11
for b₁ being Element of a₁ holds a₄ . b₁ = a₂ * ((power a₁) . b₁,a₃);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines FPower POLYNOM5:def 11 :

theorem Th65: :: POLYNOM5:65

for b₁ being non empty unital HGrStr holds FPower (1. b₁),1 = id the carrier of b₁

proof end;

theorem Th66: :: POLYNOM5:66

FPower (1. F_Complex ),2 = (id COMPLEX ) (#) (id COMPLEX )

proof end;

theorem Th67: :: POLYNOM5:67

for b₁ being non empty unital HGrStr
for b₂ being Element of b₁ holds FPower b₂,0 = the carrier of b₁ --> b₂

proof end;

theorem Th68: :: POLYNOM5:68

for b₁ being Element of F_Complex ex b₂ being Element of COMPLEX st
( b₁ = b₂ & FPower b₁,1 = b₂ (#) (id COMPLEX ) )

proof end;

theorem Th69: :: POLYNOM5:69

for b₁ being Element of F_Complex ex b₂ being Element of COMPLEX st
( b₁ = b₂ & FPower b₁,2 = b₂ (#) ((id COMPLEX ) (#) (id COMPLEX )) )

proof end;

theorem Th70: :: POLYNOM5:70

for b₁ being Element of F_Complex
for b₂ being Nat ex b₃ being Function of COMPLEX , COMPLEX st
( b₃ = FPower b₁,b₂ & FPower b₁,(b₂ + 1) = b₃ (#) (id COMPLEX ) )

proof end;

theorem Th71: :: POLYNOM5:71

for b₁ being Element of F_Complex
for b₂ being Nat ex b₃ being Function of COMPLEX , COMPLEX st
( b₃ = FPower b₁,b₂ & b₃ is_continuous_on COMPLEX )

proof end;

definition

let c₁ be non empty unital doubleLoopStr ;
let c₂ be Polynomial of c₁;
func Polynomial-Function c₁,c₂ -> Function of a₁,a₁ means :Def12: :: POLYNOM5:def 12
for b₁ being Element of a₁ holds a₃ . b₁ = eval a₂,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Polynomial-Function POLYNOM5:def 12 :

theorem Th72: :: POLYNOM5:72

for b₁ being Polynomial of F_Complex ex b₂ being Function of COMPLEX , COMPLEX st
( b₂ = Polynomial-Function F_Complex ,b₁ & b₂ is_continuous_on COMPLEX )

proof end;

theorem Th73: :: POLYNOM5:73

for b₁ being Polynomial of F_Complex st len b₁ > 2 & |.(b₁ . ((len b₁) -' 1)).| = 1 holds
for b₂ being FinSequence of REAL st len b₂ = len b₁ & ( for b₃ being Nat st b₃ in dom b₂ holds
b₂ . b₃ = |.(b₁ . (b₃ -' 1)).| ) holds
for b₃ being Element of F_Complex st |.b₃.| > Sum b₂ holds
|.(eval b₁,b₃).| > |.(b₁ . 0).| + 1

proof end;

theorem Th74: :: POLYNOM5:74

for b₁ being Polynomial of F_Complex st len b₁ > 2 holds
ex b₂ being Element of F_Complex st
for b₃ being Element of F_Complex holds |.(eval b₁,b₃).| >= |.(eval b₁,b₂).|

proof end;

theorem Th75: :: POLYNOM5:75

for b₁ being Polynomial of F_Complex st len b₁ > 1 holds
b₁ is with_roots

proof end;

registration

cluster F_Complex -> algebraic-closed ;
coherence by Def8, Th75;

end;

registration

cluster non empty associative commutative Abelian add-associative right_zeroed right_complementable right_unital distributive left_unital Field-like non degenerated algebraic-closed doubleLoopStr ;
existence

proof end;

end;