let R be domRing; :: thesis: for F being non empty FinSequence of (Polynom-Ring R)

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 (Polynom-Ring R); :: 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 S_{1}[ Nat] means for F being non empty FinSequence of (Polynom-Ring R)

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: S_{1}[ 0 ]
;

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

thus deg p = len F by I, AS; :: thesis: verum

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 (Polynom-Ring R); :: 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 S

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: 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}[b_{1} + 1] )

assume IV: S_{1}[k]
; :: thesis: S_{1}[b_{1} + 1]

end;assume IV: S

per cases
( k = 0 or k > 0 )
;

end;

suppose S:
k = 0
; :: thesis: S_{1}[b_{1} + 1]

_{1}[k + 1]
by S; :: thesis: verum

end;

now :: thesis: for F being non empty FinSequence of (Polynom-Ring R)

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

hence
Sfor 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 (Polynom-Ring R); :: 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 (Polynom-Ring R) by POLYNOM3:def 10;

F = <*q*> by A0, A, FINSEQ_1:40;

then q = p by A, GROUP_4:9;

hence deg p = 1 by HURWITZ:27; :: thesis: verum

end;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 (Polynom-Ring R) by POLYNOM3:def 10;

F = <*q*> by A0, A, FINSEQ_1:40;

then q = p by A, GROUP_4:9;

hence deg p = 1 by HURWITZ:27; :: thesis: verum

suppose S:
k > 0
; :: thesis: S_{1}[b_{1} + 1]

_{1}[k + 1]
; :: thesis: verum

end;

now :: thesis: for F being non empty FinSequence of (Polynom-Ring R)

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

hence
Sfor 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 (Polynom-Ring R); :: 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 B2, FINSEQ_1:29;

B2b: rng F c= the carrier of (Polynom-Ring R) by FINSEQ_1:def 4;

then reconsider G = G as FinSequence of (Polynom-Ring R) by B2a, XBOOLE_1:1, FINSEQ_1:def 4;

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

B3: len F = (len G) + (len <*y*>) by B2, FINSEQ_1:22

.= (len G) + 1 by FINSEQ_1:39 ;

then reconsider G = G as non empty FinSequence of (Polynom-Ring R) by S, A;

C: dom G c= dom F by B2, FINSEQ_1:26;

rng <*y*> = {y} by FINSEQ_1:39;

then G5: y in rng <*y*> by TARSKI:def 1;

rng <*y*> c= rng F by B2, FINSEQ_1:30;

then y in rng F by G5;

then reconsider y = y as Element of (Polynom-Ring R) by B2b;

dom <*y*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

then 1 in dom <*y*> by TARSKI:def 1;

then B6: F . (k + 1) = <*y*> . 1 by B2, B3, A, FINSEQ_1:def 7

.= y by FINSEQ_1:def 8 ;

dom F = Seg (k + 1) by A, FINSEQ_1:def 3;

then consider a being Element of R such that

B9: y = rpoly (1,a) by A, B6, FINSEQ_1:4;

B10: p = (Product G) * y by A, B2, GROUP_4:6

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

( q <> 0_. R & rpoly (1,a) <> 0_. R ) by F, HURWITZ:20;

hence deg p = (deg q) + (deg (rpoly (1,a))) by B10, HURWITZ:23

.= k + 1 by F, HURWITZ:27 ;

:: thesis: verum

end;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 B2, FINSEQ_1:29;

B2b: rng F c= the carrier of (Polynom-Ring R) by FINSEQ_1:def 4;

then reconsider G = G as FinSequence of (Polynom-Ring R) by B2a, XBOOLE_1:1, FINSEQ_1:def 4;

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

B3: len F = (len G) + (len <*y*>) by B2, FINSEQ_1:22

.= (len G) + 1 by FINSEQ_1:39 ;

then reconsider G = G as non empty FinSequence of (Polynom-Ring R) by S, A;

C: dom G c= dom F by B2, FINSEQ_1:26;

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

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

then F:
deg q = k
by IV, B3, A;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 B2, FINSEQ_1:def 7;

hence ex a being Element of R st G . i = rpoly (1,a) by C, C0, A; :: thesis: verum

end;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 B2, FINSEQ_1:def 7;

hence ex a being Element of R st G . i = rpoly (1,a) by C, C0, A; :: thesis: verum

rng <*y*> = {y} by FINSEQ_1:39;

then G5: y in rng <*y*> by TARSKI:def 1;

rng <*y*> c= rng F by B2, FINSEQ_1:30;

then y in rng F by G5;

then reconsider y = y as Element of (Polynom-Ring R) by B2b;

dom <*y*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;

then 1 in dom <*y*> by TARSKI:def 1;

then B6: F . (k + 1) = <*y*> . 1 by B2, B3, A, FINSEQ_1:def 7

.= y by FINSEQ_1:def 8 ;

dom F = Seg (k + 1) by A, FINSEQ_1:def 3;

then consider a being Element of R such that

B9: y = rpoly (1,a) by A, B6, FINSEQ_1:4;

B10: p = (Product G) * y by A, B2, GROUP_4:6

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

( q <> 0_. R & rpoly (1,a) <> 0_. R ) by F, HURWITZ:20;

hence deg p = (deg q) + (deg (rpoly (1,a))) by B10, HURWITZ:23

.= k + 1 by F, HURWITZ:27 ;

:: thesis: verum

thus deg p = len F by I, AS; :: thesis: verum