let R be domRing; :: thesis: for a being Element of R
for F being non empty FinSequence of () 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 () 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 (); :: 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 S1[ Nat] means for F being FinSequence of () 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: S1[1]
proof
now :: thesis: for F being FinSequence of () 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 (); :: 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 ;
then A: dom F = Seg 1 by FINSEQ_1:38;
then C: F . 1 in rng F by ;
rng F c= the carrier of () by FINSEQ_1:def 4;
then reconsider x = F . 1 as Element of the carrier of () by C;
thus p = x by
.= rpoly (1,a) by
.= (rpoly (1,a)) `^ (len F) by ; :: thesis: Roots p = {a}
then p = rpoly (1,a) by ;
hence Roots p = {a} by ro4; :: thesis: verum
end;
hence S1[1] ; :: thesis: verum
end;
IS: now :: thesis: for k being Nat st 1 <= k & S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( 1 <= k & S1[k] implies S1[k + 1] )
assume 1 <= k ; :: thesis: ( S1[k] implies S1[k + 1] )
assume IV: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for F being FinSequence of () 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 (); :: 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 (), x being Element of () such that
A1: F = G ^ <*x*> by ;
A3: F . ((len G) + 1) = x by ;
A4: len F = (len G) + () by
.= (len G) + 1 by FINSEQ_1:40 ;
len F in Seg (len F) by ;
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 ;
thus G . i = F . i by
.= 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 = () * x by
.= q *' (rpoly (1,a)) by ;
hence p = (rpoly (1,a)) `^ (len F) by ; :: thesis: Roots p = {a}
thus Roots p = () \/ (Roots (rpoly (1,a))) by
.= {a} \/ {a} by
.= {a} ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
I: for k being Nat st k >= 1 holds
S1[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