let R be domRing; :: thesis: for F being non empty FinSequence of ()
for p being Polynomial of R st 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) ) holds
deg p = len F

let F be non empty FinSequence of (); :: thesis: for p being Polynomial of R st 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) ) holds
deg p = len F

let p be Polynomial of R; :: thesis: ( 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) ) implies deg p = len F )

assume AS: ( 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) ) ) ; :: thesis: deg p = len F
defpred S1[ Nat] means for F being non empty FinSequence of ()
for p being Polynomial of R st len F = \$1 & 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) ) holds
deg p = len F;
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[b1 + 1] )
assume IV: S1[k] ; :: thesis: S1[b1 + 1]
per cases ( k = 0 or k > 0 ) ;
suppose S: k = 0 ; :: thesis: S1[b1 + 1]
now :: thesis: for F being non empty FinSequence of ()
for p being Polynomial of R st len F = 1 & 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) ) holds
deg p = 1
let F be non empty FinSequence of (); :: thesis: for p being Polynomial of R st len F = 1 & 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) ) holds
deg p = 1

let p be Polynomial of R; :: thesis: ( len F = 1 & 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) ) implies deg p = 1 )

assume A: ( len F = 1 & 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) ) ) ; :: thesis: deg p = 1
then 1 in Seg (len F) by FINSEQ_1:1;
then 1 in dom F by FINSEQ_1:def 3;
then consider a being Element of R such that
A0: F . 1 = rpoly (1,a) by A;
reconsider q = rpoly (1,a) as Element of () by POLYNOM3:def 10;
F = <*q*> by ;
then q = p by ;
hence deg p = 1 by HURWITZ:27; :: thesis: verum
end;
hence S1[k + 1] by S; :: thesis: verum
end;
suppose S: k > 0 ; :: thesis: S1[b1 + 1]
now :: thesis: for F being non empty FinSequence of ()
for p being Polynomial of R st len F = k + 1 & 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) ) holds
deg p = k + 1
let F be non empty FinSequence of (); :: thesis: for p being Polynomial of R st len F = k + 1 & 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) ) holds
deg p = k + 1

let p be Polynomial of R; :: thesis: ( len F = k + 1 & 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) ) implies deg p = k + 1 )

assume A: ( len F = k + 1 & 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) ) ) ; :: thesis: deg p = k + 1
consider G being FinSequence, y being object such that
B2: F = G ^ <*y*> by FINSEQ_1:46;
B2a: rng G c= rng F by ;
B2b: rng F c= the carrier of () by FINSEQ_1:def 4;
then reconsider G = G as FinSequence of () by ;
reconsider q = Product G as Polynomial of R by POLYNOM3:def 10;
B3: len F = (len G) + () by
.= (len G) + 1 by FINSEQ_1:39 ;
then reconsider G = G as non empty FinSequence of () by S, A;
C: dom G c= dom F by ;
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 C0: i in dom G ; :: thesis: ex a being Element of R st G . i = rpoly (1,a)
then G . i = F . i by ;
hence ex a being Element of R st G . i = rpoly (1,a) by C, C0, A; :: thesis: verum
end;
then F: deg q = k by IV, B3, A;
rng <*y*> = {y} by FINSEQ_1:39;
then G5: y in rng <*y*> by TARSKI:def 1;
rng <*y*> c= rng F by ;
then y in rng F by G5;
then reconsider y = y as Element of () by B2b;
dom <*y*> = {1} by ;
then 1 in dom <*y*> by TARSKI:def 1;
then B6: F . (k + 1) = <*y*> . 1 by
.= y by FINSEQ_1:def 8 ;
dom F = Seg (k + 1) by ;
then consider a being Element of R such that
B9: y = rpoly (1,a) by ;
B10: p = () * y by
.= q *' (rpoly (1,a)) by ;
( q <> 0_. R & rpoly (1,a) <> 0_. R ) by ;
hence deg p = (deg q) + (deg (rpoly (1,a))) by
.= k + 1 by ;
:: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
end;
end;
I: for k being Nat holds S1[k] from NAT_1:sch 2(IA, IS);
thus deg p = len F by I, AS; :: thesis: verum