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 (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: 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 (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 b2 = 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 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 (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 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 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 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 (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