:: Little {B}ezout Theorem (Factor Theorem)
:: by Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

theorem Th1: :: UPROOTS:1
for f being FinSequence of NAT st ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) holds
( Sum f = len f iff f = (len f) |-> 1 )
proofend;

scheme :: UPROOTS:sch 1
IndFinSeq0{ F1() ->  Nat, P1[ set ] } :
 for i being Element of NAT st 1 <= i &amp; i <= F1() holds
P1[i]
provided
A1: P1[1] and
A2: for i being Element of NAT st 1 <= i &amp; i < F1() &amp; P1[i] holds
P1[i + 1]
proofend;

theorem Th2: :: UPROOTS:2
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for r being FinSequence of L st len r >= 2 &amp; ( for k being Element of NAT st 2 < k &amp; k in dom r holds
r . k = 0. L ) holds
Sum r = (r /. 1) + (r /. 2)
proofend;

begin

registration
let A be finite set ;
cluster Relation-like NAT -defined A -valued Function-like one-to-one onto finite FinSequence-like FinSubsequence-like finite-support for FinSequence of A;
existence
 ex b1 being FinSequence of A st
( b1 is one-to-one &amp; b1 is onto )
proofend;
end;

definition
let A be finite set ;
func canFS A ->  FinSequence of A equals :: UPROOTS:def 1
 the one-to-one onto FinSequence of A;
coherence
 the one-to-one onto FinSequence of A is FinSequence of A ;
end;

:: deftheorem  defines canFS UPROOTS:def_1_:_
 for A being finite set holds canFS A = the one-to-one onto FinSequence of A;

registration
let A be finite set ;
cluster canFS A ->  one-to-one onto ;
coherence
 ( canFS A is one-to-one &amp; canFS A is onto ) ;
end;

theorem Th3: :: UPROOTS:3
for A being finite set holds len (canFS A) = card A
proofend;

registration
let A be non empty finite set ;
cluster canFS A ->  non empty ;
coherence
 not canFS A is empty
proofend;
end;

theorem Th4: :: UPROOTS:4
for a being set holds canFS {a} = <*a*>
proofend;

theorem Th5: :: UPROOTS:5
for A being finite set holds (canFS A) " is Function of A,(Seg (card A))
proofend;

begin

definition
let X be set ;
let S be finite Subset of X;
let n be Element of NAT ;
func(S,n) -bag  ->  Element of Bags X equals :: UPROOTS:def 2
(EmptyBag X) +* (S --> n);
correctness
coherence
(EmptyBag X) +* (S --> n) is Element of Bags X;
proofend;
end;

:: deftheorem  defines -bag UPROOTS:def_2_:_
 for X being set
for S being finite Subset of X
for n being Element of NAT holds (S,n) -bag = (EmptyBag X) +* (S --> n);

theorem Th6: :: UPROOTS:6
for X being set
for S being finite Subset of X
for n being Element of NAT
for i being set st not i in S holds
((S,n) -bag) . i = 0
proofend;

theorem Th7: :: UPROOTS:7
for X being set
for S being finite Subset of X
for n being Element of NAT
for i being set st i in S holds
((S,n) -bag) . i = n
proofend;

theorem Th8: :: UPROOTS:8
for X being set
for S being finite Subset of X
for n being Element of NAT st n <> 0 holds
support ((S,n) -bag) = S
proofend;

theorem :: UPROOTS:9
for X being set
for S being finite Subset of X
for n being Element of NAT st ( S is empty or n = 0 ) holds
(S,n) -bag = EmptyBag X
proofend;

theorem Th10: :: UPROOTS:10
for X being set
for S, T being finite Subset of X
for n being Element of NAT st S misses T holds
((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag)
proofend;

definition
let X be set ;
mode Rbag of X is real-valued finite-support ManySortedSet of X;
end;

definition
let A be set ;
let b be Rbag of A;
func Sum b ->  real number  means :Def3: :: UPROOTS:def 3
 ex f being FinSequence of REAL st
( it = Sum f &amp; f = b * (canFS (support b)) );
existence
 ex b1 being real number ex f being FinSequence of REAL st
( b1 = Sum f &amp; f = b * (canFS (support b)) )
proofend;
uniqueness
 for b1, b2 being real number st ex f being FinSequence of REAL st
( b1 = Sum f &amp; f = b * (canFS (support b)) ) &amp; ex f being FinSequence of REAL st
( b2 = Sum f &amp; f = b * (canFS (support b)) ) holds
b1 = b2 ;
end;

:: deftheorem Def3 defines Sum UPROOTS:def_3_:_
 for A being set
for b being Rbag of A
for b3 being real number holds
( b3 = Sum b iff ex f being FinSequence of REAL st
( b3 = Sum f &amp; f = b * (canFS (support b)) ) );

notation
let A be set ;
let b be bag of A;
synonym  degree b for  Sum b;
end;

definition
let A be set ;
let b be bag of A;
:: original:Sum
redefine func degree b ->  Element of NAT  means :Def4: :: UPROOTS:def 4
 ex f being FinSequence of NAT st
( it = Sum f &amp; f = b * (canFS (support b)) );
coherence
 Sum b is Element of NAT
proofend;
compatibility
 for b1 being Element of NAT holds
( b1 = Sum b iff ex f being FinSequence of NAT st
( b1 = Sum f &amp; f = b * (canFS (support b)) ) )
proofend;
end;

:: deftheorem Def4 defines degree UPROOTS:def_4_:_
 for A being set
for b being bag of A
for b3 being Element of NAT holds
( b3 = degree b iff ex f being FinSequence of NAT st
( b3 = Sum f &amp; f = b * (canFS (support b)) ) );

theorem Th11: :: UPROOTS:11
for A being set
for b being Rbag of A st b = EmptyBag A holds
Sum b = 0
proofend;

theorem Th12: :: UPROOTS:12
for A being set
for b being bag of A st Sum b = 0 holds
b = EmptyBag A
proofend;

theorem Th13: :: UPROOTS:13
for A being set
for S being finite Subset of A
for b being bag of A holds
( ( S = support b &amp; degree b = card S ) iff b = (S,1) -bag )
proofend;

theorem Th14: :: UPROOTS:14
for A being set
for S being finite Subset of A
for b being Rbag of A st support b c= S holds
ex f being FinSequence of REAL st
( f = b * (canFS S) &amp; Sum b = Sum f )
proofend;

theorem Th15: :: UPROOTS:15
for A being set
for b, b1, b2 being Rbag of A st b = b1 + b2 holds
Sum b = (Sum b1) + (Sum b2)
proofend;

theorem Th16: :: UPROOTS:16
for L being non empty unital associative commutative multMagma
for f, g being FinSequence of L
for p being Permutation of (dom f) st g = f * p holds
Product g = Product f
proofend;

begin

definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
attrp is non-zero  means :Def5: :: UPROOTS:def 5
p <> 0_. L;
end;

:: deftheorem Def5 defines non-zero UPROOTS:def_5_:_
 for L being non empty ZeroStr
for p being Polynomial of L holds
( p is non-zero iff p <> 0_. L );

theorem Th17: :: UPROOTS:17
for L being non empty ZeroStr
for p being Polynomial of L holds
( p is non-zero iff len p > 0 )
proofend;

registration
let L be non trivial ZeroStr ;
cluster Relation-like NAT -defined the carrier of L -valued Function-like non empty total quasi_total finite-Support non-zero for Element of bool [:NAT, the carrier of L:];
existence
 ex b1 being Polynomial of L st b1 is non-zero
proofend;
end;

registration
let L be non empty non degenerated multLoopStr_0 ;
let x be Element of L;
cluster<%x,(1. L)%> ->  non-zero ;
correctness
coherence
<%x,(1. L)%> is non-zero ;
proofend;
end;

theorem Th18: :: UPROOTS:18
for L being non empty ZeroStr
for p being Polynomial of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L
proofend;

theorem Th19: :: UPROOTS:19
for L being non empty ZeroStr
for p being AlgSequence of L st len p = 1 holds
( p = <%(p . 0)%> &amp; p . 0 <> 0. L )
proofend;

theorem Th20: :: UPROOTS:20
for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L holds p *' (0_. L) = 0_. L
proofend;

registration
cluster non empty non degenerated right_complementable unital associative commutative distributive Abelian add-associative right_zeroed domRing-like algebraic-closed for doubleLoopStr ;
existence
 ex b1 being non empty 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 domRing-like &amp; not b1 is degenerated )
proofend;
end;

theorem Th21: :: UPROOTS:21
for L being non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being Polynomial of L holds
( not p *' q = 0_. L or p = 0_. L or q = 0_. L )
proofend;

registration
let L be non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ;
cluster Polynom-Ring L ->  domRing-like ;
correctness
coherence
Polynom-Ring L is domRing-like ;
proofend;
end;

registration
let L be domRing;
let p, q be non-zero Polynomial of L;
clusterp *' q ->  non-zero ;
correctness
coherence
p *' q is non-zero ;
proofend;
end;

theorem :: UPROOTS:22
for L being non degenerated comRing
for p, q being Polynomial of L holds (Roots p) \/ (Roots q) c= Roots (p *' q)
proofend;

theorem Th23: :: UPROOTS:23
for L being domRing
for p, q being Polynomial of L holds Roots (p *' q) = (Roots p) \/ (Roots q)
proofend;

theorem Th24: :: UPROOTS:24
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for pc being Element of (Polynom-Ring L) st p = pc holds
- p = - pc
proofend;

theorem Th25: :: UPROOTS:25
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L
for pc, qc being Element of (Polynom-Ring L) st p = pc &amp; q = qc holds
p - q = pc - qc
proofend;

theorem Th26: :: UPROOTS:26
for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Polynomial of L holds (p *' q) - (p *' r) = p *' (q - r)
proofend;

theorem Th27: :: UPROOTS:27
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L st p - q = 0_. L holds
p = q
proofend;

theorem Th28: :: UPROOTS:28
for L being non empty right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for p, q, r being Polynomial of L st p <> 0_. L &amp; p *' q = p *' r holds
q = r
proofend;

theorem Th29: :: UPROOTS:29
for L being domRing
for n being Element of NAT
for p being Polynomial of L st p <> 0_. L holds
p `^ n <> 0_. L
proofend;

theorem Th30: :: UPROOTS:30
for L being comRing
for i, j being Element of NAT
for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j)
proofend;

theorem Th31: :: UPROOTS:31
for L being non empty multLoopStr_0 holds 1_. L = <%(1. L)%>
proofend;

theorem :: UPROOTS:32
for L being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr
for p being Polynomial of L holds p *' <%(1. L)%> = p
proofend;

theorem Th33: :: UPROOTS:33
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L st ( len p = 0 or len q = 0 ) holds
len (p *' q) = 0
proofend;

theorem Th34: :: UPROOTS:34
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L st p *' q is non-zero holds
( p is non-zero &amp; q is non-zero )
proofend;

theorem :: UPROOTS:35
for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds
0 < len (p *' q)
proofend;

theorem Th36: :: UPROOTS:36
for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being Polynomial of L st 1 < len p &amp; 1 < len q holds
len p < len (p *' q)
proofend;

theorem Th37: :: UPROOTS:37
for L being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr
for a, b being Element of L
for p being Polynomial of L holds
( (<%a,b%> *' p) . 0 = a * (p . 0) &amp; ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) )
proofend;

theorem Th38: :: UPROOTS:38
for L being non empty non degenerated right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for r being Element of L
for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1
proofend;

theorem Th39: :: UPROOTS:39
for L being non degenerated comRing
for x being Element of L
for i being Element of NAT holds len (<%x,(1. L)%> `^ i) = i + 1
proofend;

registration
let L be non degenerated comRing;
let x be Element of L;
let n be Element of NAT ;
cluster<%x,(1. L)%> `^ n ->  non-zero ;
correctness
coherence
<%x,(1. L)%> `^ n is non-zero ;
proofend;
end;

theorem Th40: :: UPROOTS:40
for L being non degenerated comRing
for x being Element of L
for q being non-zero Polynomial of L
for i being Element of NAT holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q)
proofend;

theorem Th41: :: UPROOTS:41
for L being non empty non degenerated right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for r being Element of L
for p, q being Polynomial of L st p = <%r,(1. L)%> *' q &amp; p . ((len p) -' 1) = 1. L holds
q . ((len q) -' 1) = 1. L
proofend;

begin

definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
let n be Nat;
func poly_shift (p,n) ->  Polynomial of L means :Def6: :: UPROOTS:def 6
 for i being Nat holds it . i = p . (n + i);
existence
 ex b1 being Polynomial of L st
for i being Nat holds b1 . i = p . (n + i)
proofend;
uniqueness
 for b1, b2 being Polynomial of L st ( for i being Nat holds b1 . i = p . (n + i) ) &amp; ( for i being Nat holds b2 . i = p . (n + i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines poly_shift UPROOTS:def_6_:_
 for L being non empty ZeroStr
for p being Polynomial of L
for n being Nat
for b4 being Polynomial of L holds
( b4 = poly_shift (p,n) iff for i being Nat holds b4 . i = p . (n + i) );

theorem Th42: :: UPROOTS:42
for L being non empty ZeroStr
for p being Polynomial of L holds poly_shift (p,0) = p
proofend;

theorem Th43: :: UPROOTS:43
for L being non empty ZeroStr
for n being Element of NAT
for p being Polynomial of L st n >= len p holds
poly_shift (p,n) = 0_. L
proofend;

theorem Th44: :: UPROOTS:44
for L being non empty non degenerated multLoopStr_0
for n being Element of NAT
for p being Polynomial of L st n <= len p holds
(len (poly_shift (p,n))) + n = len p
proofend;

theorem Th45: :: UPROOTS:45
for L being non degenerated comRing
for x being Element of L
for n being Element of NAT
for p being Polynomial of L st n < len p holds
eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)
proofend;

theorem Th46: :: UPROOTS:46
for L being non degenerated comRing
for p being Polynomial of L st len p = 1 holds
Roots p = {}
proofend;

definition
let L be non degenerated comRing;
let r be Element of L;
let p be Polynomial of L;
assume A1: r is_a_root_of p ;
func poly_quotient (p,r) ->  Polynomial of L means :Def7: :: UPROOTS:def 7
( (len it) + 1 = len p &amp; ( for i being Nat holds it . i = eval ((poly_shift (p,(i + 1))),r) ) ) if  len p > 0
otherwise it = 0_. L;
existence
 ( ( len p > 0 implies ex b1 being Polynomial of L st
( (len b1) + 1 = len p &amp; ( for i being Nat holds b1 . i = eval ((poly_shift (p,(i + 1))),r) ) ) ) &amp; ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L ) )
proofend;
uniqueness
 for b1, b2 being Polynomial of L holds
( ( len p > 0 &amp; (len b1) + 1 = len p &amp; ( for i being Nat holds b1 . i = eval ((poly_shift (p,(i + 1))),r) ) &amp; (len b2) + 1 = len p &amp; ( for i being Nat holds b2 . i = eval ((poly_shift (p,(i + 1))),r) ) implies b1 = b2 ) &amp; ( not len p > 0 &amp; b1 = 0_. L &amp; b2 = 0_. L implies b1 = b2 ) )
proofend;
consistency
 for b1 being Polynomial of L holds verum ;
end;

:: deftheorem Def7 defines poly_quotient UPROOTS:def_7_:_
 for L being non degenerated comRing
for r being Element of L
for p being Polynomial of L st r is_a_root_of p holds
for b4 being Polynomial of L holds
( ( len p > 0 implies ( b4 = poly_quotient (p,r) iff ( (len b4) + 1 = len p &amp; ( for i being Nat holds b4 . i = eval ((poly_shift (p,(i + 1))),r) ) ) ) ) &amp; ( not len p > 0 implies ( b4 = poly_quotient (p,r) iff b4 = 0_. L ) ) );

theorem Th47: :: UPROOTS:47
for L being non degenerated comRing
for r being Element of L
for p being non-zero Polynomial of L st r is_a_root_of p holds
len (poly_quotient (p,r)) > 0
proofend;

theorem Th48: :: UPROOTS:48
for L being non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr
for x being Element of L holds Roots <%(- x),(1. L)%> = {x}
proofend;

theorem Th49: :: UPROOTS:49
for L being non trivial comRing
for x being Element of L
for p, q being Polynomial of L st p = <%(- x),(1. L)%> *' q holds
x is_a_root_of p
proofend;

:: [WP: ] Little_Bezout_Theorem_(Factor_Theorem)
theorem Th50: :: UPROOTS:50
for L being non degenerated comRing
for r being Element of L
for p being Polynomial of L st r is_a_root_of p holds
p = <%(- r),(1. L)%> *' (poly_quotient (p,r))
proofend;

theorem :: UPROOTS:51
for L being non degenerated comRing
for r being Element of L
for p, q being Polynomial of L st p = <%(- r),(1. L)%> *' q holds
r is_a_root_of p
proofend;

Lm1: now__::_thesis:_for_L_being_domRing
for_p_being_non-zero_Polynomial_of_L_holds_
(_Roots_p_is_finite_&amp;_ex_n_being_Element_of_NAT_st_
(_n_=_card_(Roots_p)_&amp;_n_<_len_p_)_)
let L be domRing; ::_thesis: for p being non-zero Polynomial of L holds
( Roots p is finite &amp; ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p ) )
let p be non-zero Polynomial of L; ::_thesis: ( Roots p is finite &amp; ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p ) )
defpred S1[ Nat] means  for p being Polynomial of L st len p = $1 holds
( Roots p is finite &amp; ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p ) );
 p <> 0_. L by Def5;
then  len p <> 0 by POLYNOM4:5;
then A1: len p >= 0 + 1 by NAT_1:13;
A2: for n being Nat st n >= 1 &amp; S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 &amp; S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A3: S1[n] ; ::_thesis: S1[n + 1]
let p be Polynomial of L; ::_thesis: ( len p = n + 1 implies ( Roots p is finite &amp; ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p ) ) )
assume A4: len p = n + 1 ; ::_thesis: ( Roots p is finite &amp; ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p ) )
percases ( p is with_roots or not p is with_roots ) ;
suppose p is with_roots ; ::_thesis: ( Roots p is finite &amp; ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p ) )
then consider x being Element of L such that
A5: x is_a_root_of p by POLYNOM5:def_7;
set r = <%(- x),(1. L)%>;
set pq = poly_quotient (p,x);
A6: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by A5, Th50;
then A7: Roots p = (Roots <%(- x),(1. L)%>) \/ (Roots (poly_quotient (p,x))) by Th23;
A8: Roots <%(- x),(1. L)%> = {x} by Th48;
then reconsider Rr = Roots <%(- x),(1. L)%> as finite set ;
A9: (len (poly_quotient (p,x))) + 1 = len p by A4, A5, Def7;
then consider k being Element of NAT  such that
A10: k = card (Roots (poly_quotient (p,x))) and
A11: k < len (poly_quotient (p,x)) by A3, A4;
reconsider Rpq = Roots (poly_quotient (p,x)) as finite set by A3, A4, A9;
reconsider Rp = Rpq \/ Rr as finite set ;
 card Rr = 1 by A8, CARD_1:30;
then A12: card Rp <= k + 1 by A10, CARD_2:43;
 Roots (poly_quotient (p,x)) is finite by A3, A4, A9;
hence  Roots p is finite by A8, A7; ::_thesis: ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p )
take m = card Rp; ::_thesis: ( m = card (Roots p) &amp; m < len p )
thus  m = card (Roots p) by A6, Th23; ::_thesis: m < len p
 k + 1 < n + 1 by A4, A9, A11, XREAL_1:8;
hence  m < len p by A4, A12, XXREAL_0:2; ::_thesis: verum
end;
supposeA13: not p is with_roots ; ::_thesis: ( Roots p is finite &amp; ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p ) )
A14: now__::_thesis:_not_Roots_p_<>_{}
assume  Roots p <> {} ; ::_thesis: contradiction
then consider x being set  such that
A15: x in Roots p by XBOOLE_0:def_1;
reconsider x = x as Element of L by A15;
 x is_a_root_of p by A15, POLYNOM5:def_9;
hence  contradiction by A13, POLYNOM5:def_7; ::_thesis: verum
end;
hence  Roots p is finite ; ::_thesis: ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p )
take  0 ; ::_thesis: ( 0 = card (Roots p) &amp; 0 < len p )
thus  0 = card (Roots p) by A14; ::_thesis: 0 < len p
thus  0 < len p by A4; ::_thesis: verum
end;
end;
end;
A16: S1[1]
proof
let p be Polynomial of L; ::_thesis: ( len p = 1 implies ( Roots p is finite &amp; ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p ) ) )
assume A17: len p = 1 ; ::_thesis: ( Roots p is finite &amp; ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p ) )
hence  Roots p is finite by Th46; ::_thesis: ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p )
take  0 ; ::_thesis: ( 0 = card (Roots p) &amp; 0 < len p )
thus  0 = card (Roots p) by A17, Th46, CARD_1:27; ::_thesis: 0 < len p
thus  0 < len p by A17; ::_thesis: verum
end;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A16, A2);
hence  ( Roots p is finite &amp; ex n being Element of NAT st
( n = card (Roots p) &amp; n < len p ) ) by A1; ::_thesis: verum
end;

begin

registration
let L be domRing;
let p be non-zero Polynomial of L;
cluster Roots p ->  finite ;
correctness
coherence
Roots p is finite ;
by Lm1;
end;

definition
let L be non degenerated comRing;
let x be Element of L;
let p be non-zero Polynomial of L;
func multiplicity (p,x) ->  Element of NAT  means :Def8: :: UPROOTS:def 8
 ex F being non empty finite Subset of NAT st
( F =  {  k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q  }  &amp; it = max F );
existence
 ex b1 being Element of NAT ex F being non empty finite Subset of NAT st
( F =  {  k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q  }  &amp; b1 = max F )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex F being non empty finite Subset of NAT st
( F =  {  k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q  }  &amp; b1 = max F ) &amp; ex F being non empty finite Subset of NAT st
( F =  {  k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q  }  &amp; b2 = max F ) holds
b1 = b2 ;
end;

:: deftheorem Def8 defines multiplicity UPROOTS:def_8_:_
 for L being non degenerated comRing
for x being Element of L
for p being non-zero Polynomial of L
for b4 being Element of NAT holds
( b4 = multiplicity (p,x) iff ex F being non empty finite Subset of NAT st
( F =  {  k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q  }  &amp; b4 = max F ) );

theorem Th52: :: UPROOTS:52
for L being non degenerated comRing
for p being non-zero Polynomial of L
for x being Element of L holds
( x is_a_root_of p iff multiplicity (p,x) >= 1 )
proofend;

theorem Th53: :: UPROOTS:53
for L being non degenerated comRing
for x being Element of L holds multiplicity (<%(- x),(1. L)%>,x) = 1
proofend;

definition
let L be domRing;
let p be non-zero Polynomial of L;
func BRoots p ->  bag of the carrier of L means :Def9: :: UPROOTS:def 9
( support it = Roots p &amp; ( for x being Element of L holds it . x = multiplicity (p,x) ) );
existence
 ex b1 being bag of the carrier of L st
( support b1 = Roots p &amp; ( for x being Element of L holds b1 . x = multiplicity (p,x) ) )
proofend;
uniqueness
 for b1, b2 being bag of the carrier of L st support b1 = Roots p &amp; ( for x being Element of L holds b1 . x = multiplicity (p,x) ) &amp; support b2 = Roots p &amp; ( for x being Element of L holds b2 . x = multiplicity (p,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines BRoots UPROOTS:def_9_:_
 for L being domRing
for p being non-zero Polynomial of L
for b3 being bag of the carrier of L holds
( b3 = BRoots p iff ( support b3 = Roots p &amp; ( for x being Element of L holds b3 . x = multiplicity (p,x) ) ) );

theorem Th54: :: UPROOTS:54
for L being domRing
for x being Element of L holds BRoots <%(- x),(1. L)%> = ({x},1) -bag
proofend;

theorem Th55: :: UPROOTS:55
for L being domRing
for x being Element of L
for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))
proofend;

theorem Th56: :: UPROOTS:56
for L being domRing
for p, q being non-zero Polynomial of L holds BRoots (p *' q) = (BRoots p) + (BRoots q)
proofend;

Lm2: now__::_thesis:_for_L_being_domRing
for_p,_q_being_non-zero_Polynomial_of_L_holds_degree_(BRoots_(p_*'_q))_=_(degree_(BRoots_p))_+_(degree_(BRoots_q))
let L be domRing; ::_thesis: for p, q being non-zero Polynomial of L holds degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q))
let p, q be non-zero Polynomial of L; ::_thesis: degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q))
 BRoots (p *' q) = (BRoots p) + (BRoots q) by Th56;
hence  degree (BRoots (p *' q)) = (degree (BRoots p)) + (degree (BRoots q)) by Th15; ::_thesis: verum
end;

theorem Th57: :: UPROOTS:57
for L being domRing
for p being non-zero Polynomial of L st len p = 1 holds
degree (BRoots p) = 0
proofend;

theorem Th58: :: UPROOTS:58
for L being domRing
for x being Element of L
for n being Element of NAT holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n
proofend;

theorem :: UPROOTS:59
for L being algebraic-closed domRing
for p being non-zero Polynomial of L holds degree (BRoots p) = (len p) -' 1
proofend;

definition
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let c be Element of L;
let n be Element of NAT ;
func fpoly_mult_root (c,n) ->  FinSequence of (Polynom-Ring L) means :Def10: :: UPROOTS:def 10
( len it = n &amp; ( for i being Element of NAT st i in dom it holds
it . i = <%(- c),(1. L)%> ) );
existence
 ex b1 being FinSequence of (Polynom-Ring L) st
( len b1 = n &amp; ( for i being Element of NAT st i in dom b1 holds
b1 . i = <%(- c),(1. L)%> ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of (Polynom-Ring L) st len b1 = n &amp; ( for i being Element of NAT st i in dom b1 holds
b1 . i = <%(- c),(1. L)%> ) &amp; len b2 = n &amp; ( for i being Element of NAT st i in dom b2 holds
b2 . i = <%(- c),(1. L)%> ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines fpoly_mult_root UPROOTS:def_10_:_
 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for c being Element of L
for n being Element of NAT
for b4 being FinSequence of (Polynom-Ring L) holds
( b4 = fpoly_mult_root (c,n) iff ( len b4 = n &amp; ( for i being Element of NAT st i in dom b4 holds
b4 . i = <%(- c),(1. L)%> ) ) );

definition
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let b be bag of the carrier of L;
func poly_with_roots b ->  Polynomial of L means :Def11: :: UPROOTS:def 11
 ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) &amp; s = canFS (support b) &amp; ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) &amp; it = Product (FlattenSeq f) );
existence
 ex b1 being Polynomial of L ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) &amp; s = canFS (support b) &amp; ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) &amp; b1 = Product (FlattenSeq f) )
proofend;
uniqueness
 for b1, b2 being Polynomial of L st ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) &amp; s = canFS (support b) &amp; ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) &amp; b1 = Product (FlattenSeq f) ) &amp; ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) &amp; s = canFS (support b) &amp; ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) &amp; b2 = Product (FlattenSeq f) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines poly_with_roots UPROOTS:def_11_:_
 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b being bag of the carrier of L
for b3 being Polynomial of L holds
( b3 = poly_with_roots b iff ex f being FinSequence of the carrier of (Polynom-Ring L) * ex s being FinSequence of L st
( len f = card (support b) &amp; s = canFS (support b) &amp; ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) &amp; b3 = Product (FlattenSeq f) ) );

theorem Th60: :: UPROOTS:60
for L being non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr holds poly_with_roots (EmptyBag the carrier of L) = <%(1. L)%>
proofend;

theorem Th61: :: UPROOTS:61
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for c being Element of L holds poly_with_roots (({c},1) -bag) = <%(- c),(1. L)%>
proofend;

theorem Th62: :: UPROOTS:62
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b being bag of the carrier of L
for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L st len f = card (support b) &amp; s = canFS (support b) &amp; ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
len (FlattenSeq f) = degree b
proofend;

theorem Th63: :: UPROOTS:63
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b being bag of the carrier of L
for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L
for c being Element of L st len f = card (support b) &amp; s = canFS (support b) &amp; ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) &amp; ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
proofend;

theorem Th64: :: UPROOTS:64
for L being comRing
for b1, b2 being bag of the carrier of L holds poly_with_roots (b1 + b2) = (poly_with_roots b1) *' (poly_with_roots b2)
proofend;

theorem :: UPROOTS:65
for L being algebraic-closed domRing
for p being non-zero Polynomial of L st p . ((len p) -' 1) = 1. L holds
p = poly_with_roots (BRoots p)
proofend;

theorem :: UPROOTS:66
for L being comRing
for s being non empty finite Subset of L
for f being FinSequence of (Polynom-Ring L) st len f = card s &amp; ( for i being Element of NAT
for c being Element of L st i in dom f &amp; c = (canFS s) . i holds
f . i = <%(- c),(1. L)%> ) holds
poly_with_roots ((s,1) -bag) = Product f
proofend;

theorem :: UPROOTS:67
for L being non trivial comRing
for s being non empty finite Subset of L
for x being Element of L
for f being FinSequence of L st len f = card s &amp; ( for i being Element of NAT
for c being Element of L st i in dom f &amp; c = (canFS s) . i holds
f . i = eval (<%(- c),(1. L)%>,x) ) holds
eval ((poly_with_roots ((s,1) -bag)),x) = Product f
proofend;