let R be domRing; :: thesis: for a being Element of R

for F being non empty FinSequence of (Polynom-Ring R) st ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) holds

for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let a be Element of R; :: thesis: for F being non empty FinSequence of (Polynom-Ring R) st ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) holds

for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let F be non empty FinSequence of (Polynom-Ring R); :: thesis: ( ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) implies for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS1: for k being Nat st k in dom F holds

F . k = rpoly (1,a) ; :: thesis: for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let p be Polynomial of R; :: thesis: ( p = Product F implies ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS2: p = Product F ; :: thesis: ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

defpred S_{1}[ Nat] means for F being FinSequence of (Polynom-Ring R) st len F = $1 & ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) holds

for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} );

IA: S_{1}[1]

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

len F >= 1 by FINSEQ_1:20;

hence ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) by I, AS1, AS2; :: thesis: verum

for F being non empty FinSequence of (Polynom-Ring R) st ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) holds

for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let a be Element of R; :: thesis: for F being non empty FinSequence of (Polynom-Ring R) st ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) holds

for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let F be non empty FinSequence of (Polynom-Ring R); :: thesis: ( ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) implies for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS1: for k being Nat st k in dom F holds

F . k = rpoly (1,a) ; :: thesis: for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let p be Polynomial of R; :: thesis: ( p = Product F implies ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS2: p = Product F ; :: thesis: ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

defpred S

F . k = rpoly (1,a) ) holds

for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} );

IA: S

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

end;

now :: thesis: for F being FinSequence of (Polynom-Ring R) st len F = 1 & ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) holds

for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

hence
SF . k = rpoly (1,a) ) holds

for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let F be FinSequence of (Polynom-Ring R); :: thesis: ( len F = 1 & ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) implies for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS1: ( len F = 1 & ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) ) ; :: thesis: for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let p be Polynomial of R; :: thesis: ( p = Product F implies ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS2: p = Product F ; :: thesis: ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

B: F = <*(F . 1)*> by AS1, FINSEQ_1:40;

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

then C: F . 1 in rng F by FUNCT_1:3, FINSEQ_1:3;

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

then reconsider x = F . 1 as Element of the carrier of (Polynom-Ring R) by C;

thus p = x by AS2, B, GROUP_4:9

.= rpoly (1,a) by A, AS1, FINSEQ_1:3

.= (rpoly (1,a)) `^ (len F) by AS1, POLYNOM5:16 ; :: thesis: Roots p = {a}

then p = rpoly (1,a) by AS1, POLYNOM5:16;

hence Roots p = {a} by ro4; :: thesis: verum

end;F . k = rpoly (1,a) ) implies for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS1: ( len F = 1 & ( for k being Nat st k in dom F holds

F . k = rpoly (1,a) ) ) ; :: thesis: for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let p be Polynomial of R; :: thesis: ( p = Product F implies ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS2: p = Product F ; :: thesis: ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

B: F = <*(F . 1)*> by AS1, FINSEQ_1:40;

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

then C: F . 1 in rng F by FUNCT_1:3, FINSEQ_1:3;

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

then reconsider x = F . 1 as Element of the carrier of (Polynom-Ring R) by C;

thus p = x by AS2, B, GROUP_4:9

.= rpoly (1,a) by A, AS1, FINSEQ_1:3

.= (rpoly (1,a)) `^ (len F) by AS1, POLYNOM5:16 ; :: thesis: Roots p = {a}

then p = rpoly (1,a) by AS1, POLYNOM5:16;

hence Roots p = {a} by ro4; :: thesis: verum

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

S_{1}[k + 1]

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

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

assume 1 <= k ; :: 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 1 <= k ; :: thesis: ( S

assume IV: S

now :: thesis: for F being FinSequence of (Polynom-Ring R) st len F = k + 1 & ( for i being Nat st i in dom F holds

F . i = rpoly (1,a) ) holds

for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

hence
SF . i = rpoly (1,a) ) holds

for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let F be FinSequence of (Polynom-Ring R); :: thesis: ( len F = k + 1 & ( for i being Nat st i in dom F holds

F . i = rpoly (1,a) ) implies for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS1: ( len F = k + 1 & ( for i being Nat st i in dom F holds

F . i = rpoly (1,a) ) ) ; :: thesis: for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let p be Polynomial of R; :: thesis: ( p = Product F implies ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS2: p = Product F ; :: thesis: ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

consider G being FinSequence of (Polynom-Ring R), x being Element of (Polynom-Ring R) such that

A1: F = G ^ <*x*> by AS1, FINSEQ_2:19;

A3: F . ((len G) + 1) = x by A1, FINSEQ_1:42;

A4: len F = (len G) + (len <*x*>) by A1, FINSEQ_1:22

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

len F in Seg (len F) by AS1, FINSEQ_1:3;

then len F in dom F by FINSEQ_1:def 3;

then A2: x = rpoly (1,a) by AS1, A3, A4;

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

A7: p = (Product G) * x by AS2, A1, GROUP_4:6

.= q *' (rpoly (1,a)) by A2, POLYNOM3:def 10 ;

hence p = (rpoly (1,a)) `^ (len F) by A4, A6, POLYNOM5:19; :: thesis: Roots p = {a}

thus Roots p = (Roots q) \/ (Roots (rpoly (1,a))) by A7, UPROOTS:23

.= {a} \/ {a} by A6, ro4

.= {a} ; :: thesis: verum

end;F . i = rpoly (1,a) ) implies for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS1: ( len F = k + 1 & ( for i being Nat st i in dom F holds

F . i = rpoly (1,a) ) ) ; :: thesis: for p being Polynomial of R st p = Product F holds

( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

let p be Polynomial of R; :: thesis: ( p = Product F implies ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )

assume AS2: p = Product F ; :: thesis: ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )

consider G being FinSequence of (Polynom-Ring R), x being Element of (Polynom-Ring R) such that

A1: F = G ^ <*x*> by AS1, FINSEQ_2:19;

A3: F . ((len G) + 1) = x by A1, FINSEQ_1:42;

A4: len F = (len G) + (len <*x*>) by A1, FINSEQ_1:22

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

len F in Seg (len F) by AS1, FINSEQ_1:3;

then len F in dom F by FINSEQ_1:def 3;

then A2: x = rpoly (1,a) by AS1, A3, A4;

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

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

G . i = rpoly (1,a)

then A6:
( q = (rpoly (1,a)) `^ (len G) & Roots q = {a} )
by AS1, A4, IV;G . i = rpoly (1,a)

let i be Nat; :: thesis: ( i in dom G implies G . i = rpoly (1,a) )

assume A6: i in dom G ; :: thesis: G . i = rpoly (1,a)

A7: dom G c= dom F by A1, FINSEQ_1:26;

thus G . i = F . i by A1, A6, FINSEQ_1:def 7

.= rpoly (1,a) by AS1, A7, A6 ; :: thesis: verum

end;assume A6: i in dom G ; :: thesis: G . i = rpoly (1,a)

A7: dom G c= dom F by A1, FINSEQ_1:26;

thus G . i = F . i by A1, A6, FINSEQ_1:def 7

.= rpoly (1,a) by AS1, A7, A6 ; :: thesis: verum

A7: p = (Product G) * x by AS2, A1, GROUP_4:6

.= q *' (rpoly (1,a)) by A2, POLYNOM3:def 10 ;

hence p = (rpoly (1,a)) `^ (len F) by A4, A6, POLYNOM5:19; :: thesis: Roots p = {a}

thus Roots p = (Roots q) \/ (Roots (rpoly (1,a))) by A7, UPROOTS:23

.= {a} \/ {a} by A6, ro4

.= {a} ; :: thesis: verum

S

len F >= 1 by FINSEQ_1:20;

hence ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) by I, AS1, AS2; :: thesis: verum