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 S1[ Nat] means for q being Polynomial of R
for F being non empty FinSequence of () 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: S1[ 0 ] ;
IS: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume IV: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for q being Polynomial of R
for F being non empty FinSequence of () 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 () 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 b2 = 1. R

let F be non empty FinSequence of (); :: 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 b1 = 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 b1 = 1. R
then consider G being FinSequence of (), x being Element of () 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 ;
A5: x = F . (len F) by ;
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 ) ;
suppose G = {} ; :: thesis: LC b1 = 1. R
then F = <*x*> by ;
then Product F = rpoly (1,a) by ;
hence LC q = 1. R by ; :: thesis: verum
end;
suppose B1: not G is empty ; :: thesis: LC b1 = 1. R
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)
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 ;
G . i = F . i by ;
hence ex a being Element of R st G . i = rpoly (1,a) by C1, C2, AS; :: thesis: verum
end;
deg p = len G by ;
then p <> 0_. R by HURWITZ:20;
then reconsider p = p as non zero Polynomial of R by UPROOTS:def 5;
Product F = () * () by
.= () * x by GROUP_4:9
.= p *' (rpoly (1,a)) by ;
hence LC q = (LC p) * (LC (rpoly (1,a))) by
.= (LC p) * (1. R) by lcrpol
.= 1. R by AS, A4, B1, B2, IV ;
:: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
I: for k being Nat holds S1[k] from NAT_1:sch 2(IA, IS);
consider F being non empty FinSequence of () 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