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₁[ 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]

proof

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} )

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;

hence S₁[1] ; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st 1 <= k & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( 1 <= k & S₁[k] implies S₁[k + 1] )
assume 1 <= k ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

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} )

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;

now :: thesis: for i being Nat st i in dom G holds
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;

then A6: ( q = (rpoly (1,a)) `^ (len G) & Roots q = {a} ) by AS1, A4, IV;
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;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat st k >= 1 holds
S₁[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