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

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

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

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

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₂ = 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. 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. 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;

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

suppose G = {} ; :: thesis: LC b₁ = 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;

suppose B1: not G is empty ; :: thesis: LC b₁ = 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 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;

deg p = len G by B1, B2, lemppoly;
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;

end;

end;

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

end;

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