let R be domRing; :: thesis: for p being Ppoly of R holds LC p = 1. R

let p be Ppoly of R; :: thesis: LC p = 1. R

defpred S_{1}[ Nat] means for q being Polynomial of R

for F being non empty FinSequence of (Polynom-Ring R) st len F = $1 & q = Product F & ( for i being Nat st i in dom F holds

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

LC q = 1. R;

IA: S_{1}[ 0 ]
;

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

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

H: ( 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;

consider k being Nat such that

J: len F = k ;

thus LC p = 1. R by H, I, J; :: thesis: verum

let p be Ppoly of R; :: thesis: LC p = 1. R

defpred S

for F being non empty FinSequence of (Polynom-Ring R) st len F = $1 & q = Product F & ( for i being Nat st i in dom F holds

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

LC q = 1. R;

IA: S

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

S_{1}[k + 1]

I:
for k being Nat holds SS

let k be Nat; :: 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 IV: S

now :: thesis: for q being Polynomial of R

for F being non empty FinSequence of (Polynom-Ring R) st len F = k + 1 & q = Product F & ( for i being Nat st i in dom F holds

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

LC q = 1. R

hence
Sfor F being non empty FinSequence of (Polynom-Ring R) st len F = k + 1 & q = Product F & ( for i being Nat st i in dom F holds

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

LC q = 1. R

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

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

LC b_{2} = 1. R

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

ex a being Element of R st F . i = rpoly (1,a) ) implies LC b_{1} = 1. R )

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

ex a being Element of R st F . i = rpoly (1,a) ) ) ; :: thesis: LC b_{1} = 1. R

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

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

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

A4: len F = (len G) + 1 by A1, FINSEQ_2:16;

A5: x = F . (len F) by A1, A4, FINSEQ_1:42;

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

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

then consider a being Element of R such that

A2: x = rpoly (1,a) by AS, A5;

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

LC b

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

ex a being Element of R st F . i = rpoly (1,a) ) implies LC b

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

ex a being Element of R st F . i = rpoly (1,a) ) ) ; :: thesis: LC b

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

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

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

A4: len F = (len G) + 1 by A1, FINSEQ_2:16;

A5: x = F . (len F) by A1, A4, FINSEQ_1:42;

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

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

then consider a being Element of R such that

A2: x = rpoly (1,a) by AS, A5;

per cases
( G = {} or not G is empty )
;

end;

suppose
G = {}
; :: thesis: LC b_{1} = 1. R

then
F = <*x*>
by A1, FINSEQ_1:34;

then Product F = rpoly (1,a) by A2, GROUP_4:9;

hence LC q = 1. R by AS, lcrpol; :: thesis: verum

end;then Product F = rpoly (1,a) by A2, GROUP_4:9;

hence LC q = 1. R by AS, lcrpol; :: thesis: verum

suppose B1:
not G is empty
; :: thesis: LC b_{1} = 1. R

then p <> 0_. R by HURWITZ:20;

then reconsider p = p as non zero Polynomial of R by UPROOTS:def 5;

Product F = (Product G) * (Product <*x*>) by A1, GROUP_4:5

.= (Product G) * x by GROUP_4:9

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

hence LC q = (LC p) * (LC (rpoly (1,a))) by AS, NIVEN:46

.= (LC p) * (1. R) by lcrpol

.= 1. R by AS, A4, B1, B2, IV ;

:: thesis: verum

end;

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

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

deg p = len G
by B1, B2, lemppoly;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 C1: i in dom G ; :: thesis: ex a being Element of R st G . i = rpoly (1,a)

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

G . i = F . i by A1, C1, FINSEQ_1:def 7;

hence ex a being Element of R st G . i = rpoly (1,a) by C1, C2, AS; :: thesis: verum

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

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

G . i = F . i by A1, C1, FINSEQ_1:def 7;

hence ex a being Element of R st G . i = rpoly (1,a) by C1, C2, AS; :: thesis: verum

then p <> 0_. R by HURWITZ:20;

then reconsider p = p as non zero Polynomial of R by UPROOTS:def 5;

Product F = (Product G) * (Product <*x*>) by A1, GROUP_4:5

.= (Product G) * x by GROUP_4:9

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

hence LC q = (LC p) * (LC (rpoly (1,a))) by AS, NIVEN:46

.= (LC p) * (1. R) by lcrpol

.= 1. R by AS, A4, B1, B2, IV ;

:: thesis: verum

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

H: ( 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;

consider k being Nat such that

J: len F = k ;

thus LC p = 1. R by H, I, J; :: thesis: verum