let F be Field; :: thesis:
let G be non empty FinSequence of the carrier of (Polynom-Ring F); :: thesis:
let q be non constant Polynomial of F; :: thesis:
assume AS: q = Product G ; :: thesis:

A: now :: thesis:

assume A1: q splits_in F ; :: thesis:

now :: thesis:

let i be Element of dom G; :: thesis:
let p be Polynomial of F; :: thesis:
assume H2: p = G . i ; :: thesis:
H5: G . i = G /. i by PARTFUN1:def 6;
then H4: p = Product <*(G /. i)*> by H2, GROUP_4:9;
reconsider r1 = Product (G | (i -' 1)), r2 = Product (G /^ i) as Polynomial of F by POLYNOM3:def 10;
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 H9: 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 -' 1))) * (Product <*(G . i)*>) = r1 *' p by H4, H5, POLYNOM3:def 10;
then q = (p *' r1) *' r2 by AS, H9, POLYNOM3:def 10
.= p *' (r1 *' r2) by POLYNOM3:33 ;
then ( not r1 *' r2 is zero & p *' (r1 *' r2) splits_in F ) by A1;
hence ( p is constant or p splits_in F ) by FIELD_8:11; :: thesis:

end;

hence for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in F ) ; :: thesis:

end;

now :: thesis:

assume C: for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in F ) ; :: thesis:
defpred S₁[ Nat] means for G being FinSequence of the carrier of (Polynom-Ring F) st len G = $1 holds
for q being non constant Polynomial of F st q = Product G & ( for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in F ) ) holds
q splits_in F;
A: S₁[ 0 ]

proof

now :: thesis:

let G be FinSequence of the carrier of (Polynom-Ring F); :: thesis:
assume A0: len G = 0 ; :: thesis:
let q be non constant Polynomial of F; :: thesis:
assume A1: ( q = Product G & ( for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in F ) ) ) ; :: thesis:
G = <*> the carrier of (Polynom-Ring F) by A0;
then Product G = 1_ (Polynom-Ring F) by GROUP_4:8
.= 1_. F by POLYNOM3:def 10 ;
hence q splits_in F by A1; :: thesis:

end;

hence S₁[ 0 ] ; :: thesis:

end;

B: now :: thesis:

let k be Nat; :: thesis:
assume IV: S₁[k] ; :: thesis:

now :: thesis:

let G be FinSequence of the carrier of (Polynom-Ring F); :: thesis:
assume B0: len G = k + 1 ; :: thesis:
let q be non constant Polynomial of F; :: thesis:
assume B1: ( q = Product G & ( for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in F ) ) ) ; :: thesis:
G <> {} by B0;
then consider G1 being FinSequence, y being object such that
B2: G = G1 ^ <*y*> by FINSEQ_1:46;
H: rng G c= the carrier of (Polynom-Ring F) by FINSEQ_1:def 4;
rng G1 c= rng G by B2, FINSEQ_1:29;
then reconsider G1 = G1 as FinSequence of the carrier of (Polynom-Ring F) by XBOOLE_1:1, H, FINSEQ_1:def 4;
reconsider r = Product G1 as Polynomial of F by POLYNOM3:def 10;
len <*y*> = 1 by FINSEQ_1:40;
then C4: dom G = Seg ((len G1) + 1) by B2, FINSEQ_1:def 7;
B12: 1 <= (len G1) + 1 by NAT_1:11;
dom <*y*> = Seg 1 by FINSEQ_1:38;
then B11: 1 in dom <*y*> by FINSEQ_1:3;
y = <*y*> . 1
.= G . ((len G1) + 1) by B11, B2, FINSEQ_1:def 7 ;
then B13: y in rng G by B12, C4, FINSEQ_1:1, FUNCT_1:3;
rng G c= the carrier of (Polynom-Ring F) by FINSEQ_1:def 4;
then reconsider y = y as Element of the carrier of (Polynom-Ring F) by B13;
set G2 = <*y*>;
reconsider p = Product <*y*> as Polynomial of F by POLYNOM3:def 10;
reconsider p1 = p, r1 = r as Element of the carrier of (Polynom-Ring F) ;
B3: q = (Product G1) * y by B1, B2, GROUP_4:6
.= r1 * p1 by GROUP_4:9
.= r *' p by POLYNOM3:def 10 ;
B4: len G = (len G1) + (len <*y*>) by B2, FINSEQ_1:22
.= (len G1) + 1 by FINSEQ_1:39 ;

per cases ;

suppose dom G1 = {} ; :: thesis:

then V4: G1 = {} ;
then V2: G = <*y*> by B2, FINSEQ_1:34;
V1: y = <*y*> . 1
.= G . ((len G1) + 1) by B11, B2, FINSEQ_1:def 7 ;
dom G = Seg 1 by V2, FINSEQ_1:38;
then (len G1) + 1 in dom G by V4, FINSEQ_1:1;
hence q splits_in F by B1, V1, V2, GROUP_4:9; :: thesis:

end;

suppose V: dom G1 <> {} ; :: thesis:

B6: now :: thesis:

let i be Element of dom G1; :: thesis:
let p be Polynomial of F; :: thesis:
assume p = G1 . i ; :: thesis:
then B7: p = G . i by V, B2, FINSEQ_1:def 7;
dom G1 c= dom G by B2, FINSEQ_1:26;
then i in dom G by V;
hence ( p is constant or p splits_in F ) by B1, B7; :: thesis:

end;

B10: now :: thesis:

let i be Element of dom <*y*>; :: thesis:
let p be Polynomial of F; :: thesis:
assume p = <*y*> . i ; :: thesis:
then C2: p = G . ((len G1) + i) by B2, FINSEQ_1:def 7;
dom <*y*> = {1} by FINSEQ_1:38, FINSEQ_1:2;
then C3: i = 1 by TARSKI:def 1;
len <*y*> = 1 by FINSEQ_1:40;
then C4: dom G = Seg ((len G1) + 1) by B2, FINSEQ_1:def 7;
1 <= (len G1) + 1 by NAT_1:11;
then (len G1) + i in dom G by C4, C3, FINSEQ_1:1;
hence ( p is constant or p splits_in F ) by B1, C2; :: thesis:

end;

dom <*y*> = Seg 1 by FINSEQ_1:38;
then B11: 1 in dom <*y*> by FINSEQ_1:3;
<*y*> . 1 = y
.= p by GROUP_4:9 ;

per cases by B10, B11;

suppose C: p is constant ; :: thesis:

then deg p <= 0 by RATFUNC1:def 2;
then consider b being Element of F such that
B9: p1 = b | F by RING_4:20, RING_4:def 4;
b <> 0. F by B3, B9;
then reconsider b = b as non zero Element of F by STRUCT_0:def 12;

per cases ;

suppose not r is constant ; :: thesis:

then consider a being non zero Element of F, u being Ppoly of F such that
B8: r = a * u by B0, B4, B6, IV, FIELD_4:def 5;
q = (b * (1_. F)) *' (a * u) by B3, B8, B9, RING_4:16
.= b * ((a * u) *' (1_. F)) by RING_4:10
.= (b * a) * u by RING_4:11 ;
hence q splits_in F by FIELD_4:def 5; :: thesis:

end;

suppose r is constant ; :: thesis:

hence q splits_in F by C, B3; :: thesis:

end;

suppose C1: p splits_in F ; :: thesis:

per cases ;

suppose not r is constant ; :: thesis:

then r splits_in F by B4, B6, B0, IV;
hence q splits_in F by B3, C1, FIELD_8:12; :: thesis:

end;

suppose r is constant ; :: thesis:

then deg r <= 0 by RATFUNC1:def 2;
then consider b being Element of F such that
C2: r1 = b | F by RING_4:20, RING_4:def 4;
b <> 0. F by B3, C2;
then reconsider b = b as non zero Element of F by STRUCT_0:def 12;
consider a being non zero Element of F, u being Ppoly of F such that
C3: p = a * u by C1, FIELD_4:def 5;
q = (a * u) *' (b * (1_. F)) by B3, C3, C2, RING_4:16
.= b * ((a * u) *' (1_. F)) by RING_4:10
.= (b * a) * u by RING_4:11 ;
hence q splits_in F by FIELD_4:def 5; :: thesis:

end;

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

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);
consider n being Nat such that
H: len G = n ;
thus q splits_in F by C, I, H, AS; :: thesis:

end;

hence ( q splits_in F iff for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in F ) ) by A; :: thesis: