let R be domRing; :: thesis: for p being Ppoly of R holds p is Ppoly of R, BRoots p

let p be Ppoly of R; :: thesis: p is Ppoly of R, BRoots p

defpred S_{1}[ Nat] means for p being Ppoly of R st deg p = $1 holds

p is Ppoly of R, BRoots p;

IA: S_{1}[1]

S_{1}[k]
from NAT_1:sch 8(IA, IS);

reconsider n = deg p as Element of NAT by INT_1:3;

n + 1 > 0 + 1 by RATFUNC1:def 2, XREAL_1:6;

then n >= 1 by NAT_1:13;

hence p is Ppoly of R, BRoots p by I; :: thesis: verum

let p be Ppoly of R; :: thesis: p is Ppoly of R, BRoots p

defpred S

p is Ppoly of R, BRoots p;

IA: S

proof
_{1}[1]
; :: thesis: verum

end;

now :: thesis: for p being Ppoly of R st deg p = 1 holds

p is Ppoly of R, BRoots p

hence
Sp is Ppoly of R, BRoots p

let p be Ppoly of R; :: thesis: ( deg p = 1 implies p is Ppoly of R, BRoots p )

assume A0: deg p = 1 ; :: thesis: p is Ppoly of R, BRoots p

consider F being non empty FinSequence of (Polynom-Ring R) such that

A1: ( p = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) ) by dpp1;

len F = 1 by A0, A1, lemppoly;

then A2: F = <*(F . 1)*> by FINSEQ_1:40;

then A3: dom F = Seg 1 by FINSEQ_1:38;

then consider a being Element of R such that

A4: F . 1 = rpoly (1,a) by A1, FINSEQ_1:1;

reconsider e = 1 as Element of dom F by A3, FINSEQ_1:1;

A5: Product F = F . e by A2, GROUP_4:9;

rpoly (1,a) = <%(- a),(1. R)%> by repr;

then BRoots (rpoly (1,a)) = Bag {a} by UPROOTS:54;

hence p is Ppoly of R, BRoots p by A1, A4, A5, lemacf; :: thesis: verum

end;assume A0: deg p = 1 ; :: thesis: p is Ppoly of R, BRoots p

consider F being non empty FinSequence of (Polynom-Ring R) such that

A1: ( p = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) ) by dpp1;

len F = 1 by A0, A1, lemppoly;

then A2: F = <*(F . 1)*> by FINSEQ_1:40;

then A3: dom F = Seg 1 by FINSEQ_1:38;

then consider a being Element of R such that

A4: F . 1 = rpoly (1,a) by A1, FINSEQ_1:1;

reconsider e = 1 as Element of dom F by A3, FINSEQ_1:1;

A5: Product F = F . e by A2, GROUP_4:9;

rpoly (1,a) = <%(- a),(1. R)%> by repr;

then BRoots (rpoly (1,a)) = Bag {a} by UPROOTS:54;

hence p is Ppoly of R, BRoots p by A1, A4, A5, lemacf; :: thesis: verum

IS: now :: thesis: for k being Nat st k >= 1 & S_{1}[k] holds

S_{1}[k + 1]

I:
for k being Nat st k >= 1 holds S

let k be Nat; :: thesis: ( k >= 1 & S_{1}[k] implies S_{1}[k + 1] )

assume AS: k >= 1 ; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume IV: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume AS: k >= 1 ; :: thesis: ( S

assume IV: S

now :: thesis: for p being Ppoly of R st deg p = k + 1 holds

p is Ppoly of R, BRoots p

hence
Sp is Ppoly of R, BRoots p

let p be Ppoly of R; :: thesis: ( deg p = k + 1 implies p is Ppoly of R, BRoots p )

assume B0: deg p = k + 1 ; :: thesis: p is Ppoly of R, BRoots p

consider F being non empty FinSequence of (Polynom-Ring R) such that

B1: ( p = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) ) by dpp1;

B1a: len F = k + 1 by B0, B1, lemppoly;

consider G being FinSequence, y being object such that

B2: F = G ^ <*y*> by FINSEQ_1:46;

B2a: rng G c= rng F by B2, FINSEQ_1:29;

B2b: rng F c= the carrier of (Polynom-Ring R) by FINSEQ_1:def 4;

then reconsider G = G as FinSequence of (Polynom-Ring R) by B2a, XBOOLE_1:1, FINSEQ_1:def 4;

B3: len F = (len G) + (len <*y*>) by B2, FINSEQ_1:22

.= (len G) + 1 by FINSEQ_1:39 ;

then reconsider G = G as non empty FinSequence of (Polynom-Ring R) by B1a, AS;

reconsider q = Product G as Polynomial of R by POLYNOM3:def 10;

C: dom G c= dom F by B2, FINSEQ_1:26;

set B = BRoots q;

deg q = k by B1a, B3, D, lemppoly;

then reconsider q = q as Ppoly of R, BRoots q by IV;

rng <*y*> = {y} by FINSEQ_1:39;

then G5: y in rng <*y*> by TARSKI:def 1;

rng <*y*> c= rng F by B2, FINSEQ_1:30;

then y in rng F by G5;

then reconsider y = y as Element of (Polynom-Ring R) by B2b;

dom <*y*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

then 1 in dom <*y*> by TARSKI:def 1;

then B6: F . (k + 1) = <*y*> . 1 by B2, B3, B1a, FINSEQ_1:def 7

.= y by FINSEQ_1:def 8 ;

dom F = Seg (k + 1) by B1a, FINSEQ_1:def 3;

then consider a being Element of R such that

B9: y = rpoly (1,a) by B1, B6, FINSEQ_1:4;

reconsider r = y as Ppoly of R, Bag {a} by lemacf, B9;

B10: p = (Product G) * y by B1, B2, GROUP_4:6

.= q *' r by POLYNOM3:def 10 ;

reconsider B1 = (BRoots q) + (Bag {a}) as non zero bag of the carrier of R ;

rpoly (1,a) = <%(- a),(1. R)%> by repr;

then BRoots (rpoly (1,a)) = Bag {a} by UPROOTS:54;

then BRoots p = (BRoots q) + (Bag {a}) by B9, B10, UPROOTS:56;

hence p is Ppoly of R, BRoots p by B10, lemacf2; :: thesis: verum

end;assume B0: deg p = k + 1 ; :: thesis: p is Ppoly of R, BRoots p

consider F being non empty FinSequence of (Polynom-Ring R) such that

B1: ( p = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) ) by dpp1;

B1a: len F = k + 1 by B0, B1, lemppoly;

consider G being FinSequence, y being object such that

B2: F = G ^ <*y*> by FINSEQ_1:46;

B2a: rng G c= rng F by B2, FINSEQ_1:29;

B2b: rng F c= the carrier of (Polynom-Ring R) by FINSEQ_1:def 4;

then reconsider G = G as FinSequence of (Polynom-Ring R) by B2a, XBOOLE_1:1, FINSEQ_1:def 4;

B3: len F = (len G) + (len <*y*>) by B2, FINSEQ_1:22

.= (len G) + 1 by FINSEQ_1:39 ;

then reconsider G = G as non empty FinSequence of (Polynom-Ring R) by B1a, AS;

reconsider q = Product G as Polynomial of R by POLYNOM3:def 10;

C: dom G c= dom F by B2, FINSEQ_1:26;

D: now :: thesis: for i being Nat st i in dom G holds

ex a being Element of R st G . i = rpoly (1,a)

then reconsider q = q as Ppoly of R by dpp1;ex a being Element of R st G . i = rpoly (1,a)

let i be Nat; :: thesis: ( i in dom G implies ex a being Element of R st G . i = rpoly (1,a) )

assume C0: i in dom G ; :: thesis: ex a being Element of R st G . i = rpoly (1,a)

then G . i = F . i by B2, FINSEQ_1:def 7;

hence ex a being Element of R st G . i = rpoly (1,a) by C, C0, B1; :: thesis: verum

end;assume C0: i in dom G ; :: thesis: ex a being Element of R st G . i = rpoly (1,a)

then G . i = F . i by B2, FINSEQ_1:def 7;

hence ex a being Element of R st G . i = rpoly (1,a) by C, C0, B1; :: thesis: verum

set B = BRoots q;

deg q = k by B1a, B3, D, lemppoly;

then reconsider q = q as Ppoly of R, BRoots q by IV;

rng <*y*> = {y} by FINSEQ_1:39;

then G5: y in rng <*y*> by TARSKI:def 1;

rng <*y*> c= rng F by B2, FINSEQ_1:30;

then y in rng F by G5;

then reconsider y = y as Element of (Polynom-Ring R) by B2b;

dom <*y*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

then 1 in dom <*y*> by TARSKI:def 1;

then B6: F . (k + 1) = <*y*> . 1 by B2, B3, B1a, FINSEQ_1:def 7

.= y by FINSEQ_1:def 8 ;

dom F = Seg (k + 1) by B1a, FINSEQ_1:def 3;

then consider a being Element of R such that

B9: y = rpoly (1,a) by B1, B6, FINSEQ_1:4;

reconsider r = y as Ppoly of R, Bag {a} by lemacf, B9;

B10: p = (Product G) * y by B1, B2, GROUP_4:6

.= q *' r by POLYNOM3:def 10 ;

reconsider B1 = (BRoots q) + (Bag {a}) as non zero bag of the carrier of R ;

rpoly (1,a) = <%(- a),(1. R)%> by repr;

then BRoots (rpoly (1,a)) = Bag {a} by UPROOTS:54;

then BRoots p = (BRoots q) + (Bag {a}) by B9, B10, UPROOTS:56;

hence p is Ppoly of R, BRoots p by B10, lemacf2; :: thesis: verum

S

reconsider n = deg p as Element of NAT by INT_1:3;

n + 1 > 0 + 1 by RATFUNC1:def 2, XREAL_1:6;

then n >= 1 by NAT_1:13;

hence p is Ppoly of R, BRoots p by I; :: thesis: verum