let F be Field; :: thesis: for G being non empty FinSequence of the carrier of (Polynom-Ring F) st ( for i being Element of dom G holds G . i <> 0_. F ) holds
for q being Polynomial of F st q = Product G holds
for i being Element of dom G
for p being Polynomial of F st p = G . i holds
deg p <= deg q
let G be non empty FinSequence of the carrier of (Polynom-Ring F); :: thesis: ( ( for i being Element of dom G holds G . i <> 0_. F ) implies for q being Polynomial of F st q = Product G holds
for i being Element of dom G
for p being Polynomial of F st p = G . i holds
deg p <= deg q )
assume AS: for i being Element of dom G holds G . i <> 0_. F ; :: thesis: for q being Polynomial of F st q = Product G holds
for i being Element of dom G
for p being Polynomial of F st p = G . i holds
deg p <= deg q
let q be Polynomial of F; :: thesis: ( q = Product G implies for i being Element of dom G
for p being Polynomial of F st p = G . i holds
deg p <= deg q )
assume A: q = Product G ; :: thesis: for i being Element of dom G
for p being Polynomial of F st p = G . i holds
deg p <= deg q
let i be Element of dom G; :: thesis: for p being Polynomial of F st p = G . i holds
deg p <= deg q
let p be Polynomial of F; :: thesis: ( p = G . i implies deg p <= deg q )
assume B: p = G . i ; :: thesis: deg p <= deg q
dom G = Seg (len G) by FINSEQ_1:def 3;
then ( 1 <= i & i <= len G ) by FINSEQ_1:1;
then G = ((G | (i -' 1)) ^ <*(G . i)*>) ^ (G /^ i) by FINSEQ_5:84;
then D: Product G = (Product ((G | (i -' 1)) ^ <*(G . i)*>)) * (Product (G /^ i)) by GROUP_4:5
.= ((Product (G | (i -' 1))) * (Product <*(G . i)*>)) * (Product (G /^ i)) by GROUP_4:5
.= ((Product <*(G . i)*>) * (Product (G | (i -' 1)))) * (Product (G /^ i)) by GROUP_1:def 12
.= (Product <*(G . i)*>) * ((Product (G | (i -' 1))) * (Product (G /^ i))) by GROUP_1:def 3 ;
reconsider r1 = Product (G | (i -' 1)), r2 = Product (G /^ i) as Polynomial of F by POLYNOM3:def 10;
I: G . i = G /. i by PARTFUN1:def 6;
then E: Product <*(G /. i)*> = p by B, GROUP_4:9;
Z: r1 *' r2 = (Product (G | (i -' 1))) * (Product (G /^ i)) by POLYNOM3:def 10;
then F: q = p *' (r1 *' r2) by A, D, E, I, POLYNOM3:def 10;
G1: r1 *' r2 = Product ((G | (i -' 1)) ^ (G /^ i)) by Z, GROUP_4:5;

per cases ( (G | (i -' 1)) ^ (G /^ i) = {} or (G | (i -' 1)) ^ (G /^ i) <> {} ) ;

suppose (G | (i -' 1)) ^ (G /^ i) = {} ; :: thesis: deg p <= deg q

then (G | (i -' 1)) ^ (G /^ i) = <*> the carrier of (Polynom-Ring F) ;
then Product ((G | (i -' 1)) ^ (G /^ i)) = 1_ (Polynom-Ring F) by GROUP_4:8
.= 1_. F by POLYNOM3:def 10 ;
hence deg p <= deg q by F, G1; :: thesis: verum

end;

suppose S: (G | (i -' 1)) ^ (G /^ i) <> {} ; :: thesis: deg p <= deg q

G: r1 *' r2 <> 0_. F

proof

now :: thesis: for j being Element of dom ((G | (i -' 1)) ^ (G /^ i)) holds ((G | (i -' 1)) ^ (G /^ i)) . j <> 0_. F

let j be Element of dom ((G | (i -' 1)) ^ (G /^ i)); :: thesis: ((G | (i -' 1)) ^ (G /^ i)) . b₁ <> 0_. F

per cases ( j in dom (G | (i -' 1)) or ex n being Nat st
( n in dom (G /^ i) & j = (len (G | (i -' 1))) + n ) ) by S, FINSEQ_1:25;

suppose T: j in dom (G | (i -' 1)) ; :: thesis: ((G | (i -' 1)) ^ (G /^ i)) . b₁ <> 0_. F

G3: G | (i -' 1) = G | (Seg (i -' 1)) by FINSEQ_1:def 16;
G2: dom (G | (i -' 1)) c= dom G by FINSEQ_5:18;
((G | (i -' 1)) ^ (G /^ i)) . j = (G | (i -' 1)) . j by T, FINSEQ_1:def 7
.= G . j by T, G3, FUNCT_1:47 ;
hence ((G | (i -' 1)) ^ (G /^ i)) . j <> 0_. F by T, G2, AS; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom (G /^ i) & j = (len (G | (i -' 1))) + n ) ; :: thesis: ((G | (i -' 1)) ^ (G /^ i)) . b₁ <> 0_. F

then consider n being Nat such that
G2: ( n in dom (G /^ i) & j = (len (G | (i -' 1))) + n ) ;
G3: i + n in dom G by G2, FINSEQ_5:26;
((G | (i -' 1)) ^ (G /^ i)) . j = (G /^ i) . n by G2, FINSEQ_1:def 7
.= G . (i + n) by G2, FINSEQ_5:27 ;
hence ((G | (i -' 1)) ^ (G /^ i)) . j <> 0_. F by G3, AS; :: thesis: verum

end;

end;

end;

hence r1 *' r2 <> 0_. F by S, G1, lemNor1dega; :: thesis: verum

end;

then H: deg (r1 *' r2) is Nat by T8;
p <> 0_. F by B, AS;
then deg q = (deg p) + (deg (r1 *' r2)) by F, G, HURWITZ:23;
hence deg p <= deg q by H, INT_1:6; :: thesis: verum

end;

end;