let F be Field; :: thesis: for f being non constant Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st f splits_in E
let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ex E being FieldExtension of F st f splits_in E
defpred S₁[ Nat] means for F being Field
for f being non constant Element of the carrier of (Polynom-Ring F) st deg f = $1 holds
ex E being FieldExtension of F st f splits_in E;
IA: S₁[1]

proof

let F be Field; :: thesis: for f being non constant Element of the carrier of (Polynom-Ring F) st deg f = 1 holds
ex E being FieldExtension of F st f splits_in E
let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( deg f = 1 implies ex E being FieldExtension of F st f splits_in E )
assume A: deg f = 1 ; :: thesis: ex E being FieldExtension of F st f splits_in E
reconsider E = F as FieldExtension of F by FIELD_4:6;
take E ; :: thesis: f splits_in E
thus f splits_in E by FIELD_4:29, A; :: thesis: verum

end;

IS: now :: thesis: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for F being Field
for f being non constant Element of the carrier of (Polynom-Ring F) st deg f = k + 1 holds
ex E being FieldExtension of F st f splits_in E

let F be Field; :: thesis: for f being non constant Element of the carrier of (Polynom-Ring F) st deg f = k + 1 holds
ex E being FieldExtension of E st b₃ splits_in b₄
let f be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( deg f = k + 1 implies ex E being FieldExtension of E st b₂ splits_in b₃ )
assume AS2: deg f = k + 1 ; :: thesis: ex E being FieldExtension of E st b₂ splits_in b₃
consider E1 being FieldExtension of F such that
A: f is_with_roots_in E1 by main;
reconsider f1 = f as Polynomial of E1 by FIELD_4:8;
reconsider f1 = f1 as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;
consider a being Element of E1 such that
B: a is_a_root_of f,E1 by A, FIELD_4:def 3;
reconsider h = rpoly (1,a) as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;
reconsider q = rpoly (1,a) as Ppoly of E1 by RING_5:51;
Ext_eval (f,a) = 0. E1 by B, FIELD_4:def 2;
then 0. E1 = eval (f1,a) by FIELD_4:26;
then consider g2 being Polynomial of E1 such that
C1: f1 = h *' g2 by RING_4:1, RING_5:11;
reconsider g = g2 as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;
C: f1 = h * g by C1, POLYNOM3:def 10;

per cases ( g is constant or not g is constant ) ;

suppose g is constant ; :: thesis: ex E being FieldExtension of E st b₂ splits_in b₃

then consider e being Element of E1 such that
D: g = e | E1 by RING_4:20;

now :: thesis: not e is zero

assume e is zero ; :: thesis: contradiction
then g = 0_. E1 by D, RING_4:13;
then f = 0_. F by C1, FIELD_4:12;
hence contradiction ; :: thesis: verum

end;

then reconsider e = e as non zero Element of E1 ;
f = (rpoly (1,a)) *' (e * (1_. E1)) by D, C1, RING_4:16
.= e * ((rpoly (1,a)) *' (1_. E1)) by RING_4:10
.= e * q ;
hence ex E being FieldExtension of F st f splits_in E by FIELD_4:def 5; :: thesis: verum

end;

suppose I: not g is constant ; :: thesis: ex E being FieldExtension of E st b₂ splits_in b₃

deg g = k

proof

reconsider g1 = g as Polynomial of E1 ;
g1 <> 0_. E1 by I;
then D: deg f1 = (deg (rpoly (1,a))) + (deg g1) by C1, HURWITZ:23
.= 1 + (deg g1) by HURWITZ:27 ;
deg f1 = k + 1 by AS2, FIELD_4:20;
hence deg g = k by D; :: thesis: verum

end;

then consider E2 being FieldExtension of E1 such that
E: g splits_in E2 by I, IV;
reconsider E2 = E2 as FieldExtension of F ;
consider e being non zero Element of E2, r being Ppoly of E2 such that
F: g = e * r by E, FIELD_4:def 5;
E1 is Subring of E2 by FIELD_4:def 1;
then the carrier of E1 c= the carrier of E2 by C0SP1:def 3;
then reconsider a1 = a as Element of E2 ;
rpoly (1,a1) is Ppoly of E2 by RING_5:51;
then reconsider u = (rpoly (1,a1)) *' r as Ppoly of E2 by RING_5:52;
reconsider q = rpoly (1,a) as Polynomial of E2 by FIELD_4:8;
reconsider q1 = q as Element of the carrier of (Polynom-Ring E2) by POLYNOM3:def 10;
reconsider eg = e * r as Element of the carrier of (Polynom-Ring E2) by POLYNOM3:def 10;
Y: q = rpoly (1,a1) by FIELD_4:21;
Z1: [h,g] in [: the carrier of (Polynom-Ring E1), the carrier of (Polynom-Ring E1):] by ZFMISC_1:def 2;
the multF of (Polynom-Ring E2) || the carrier of (Polynom-Ring E1) = the multF of (Polynom-Ring E1) by FIELD_4:18;
then f = q1 * eg by F, C, Z1, FUNCT_1:49
.= q *' (e * r) by POLYNOM3:def 10
.= e * u by Y, RING_4:10 ;
hence ex E being FieldExtension of F st f splits_in E by FIELD_4:def 5; :: thesis: verum

end;

end;

end;

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

end;

I: for k being non zero Nat holds S₁[k] from NAT_1:sch 10(IA, IS);
consider n being Nat such that
H: deg f = n ;
n + 1 > 0 + 1 by H, RING_4:def 4, XREAL_1:6;
hence ex E being FieldExtension of F st f splits_in E by I, H; :: thesis: verum