let F be Field; :: thesis: for P being finite Subset of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E
let P be finite Subset of the carrier of (Polynom-Ring F); :: thesis: ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E
defpred S₁[ Nat] means for F being Field
for P being finite Subset of the carrier of (Polynom-Ring F) st card P = $1 holds
ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E;
IA: S₁[ 0 ]

proof

now :: thesis: for F being Field
for P being finite Subset of the carrier of (Polynom-Ring F) st card P = 0 holds
ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E

let F be Field; :: thesis: for P being finite Subset of the carrier of (Polynom-Ring F) st card P = 0 holds
ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E
let P be finite Subset of the carrier of (Polynom-Ring F); :: thesis: ( card P = 0 implies ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E )
assume A: card P = 0 ; :: thesis: ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E
reconsider E = F as FieldExtension of F by FIELD_4:6;
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E by A;
hence ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E ; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

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

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

now :: thesis: for F being Field
for P being finite Subset of the carrier of (Polynom-Ring F) st card P = k + 1 holds
ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E

let F be Field; :: thesis: for P being finite Subset of the carrier of (Polynom-Ring F) st card P = k + 1 holds
ex E being FieldExtension of E st
for p being non constant Element of the carrier of (Polynom-Ring E) st b₅ in p holds
b₅ is_with_roots_in b₄
let P be finite Subset of the carrier of (Polynom-Ring F); :: thesis: ( card P = k + 1 implies ex E being FieldExtension of E st
for p being non constant Element of the carrier of (Polynom-Ring E) st b₄ in p holds
b₄ is_with_roots_in b₃ )
assume AS: card P = k + 1 ; :: thesis: ex E being FieldExtension of E st
for p being non constant Element of the carrier of (Polynom-Ring E) st b₄ in p holds
b₄ is_with_roots_in b₃
set p = the Element of P;
set B = P \ { the Element of P};
P <> {} by AS;
then B3: ( the Element of P in P & the Element of P in { the Element of P} ) by TARSKI:def 1;
then B1: not the Element of P in P \ { the Element of P} by XBOOLE_0:def 5;
{ the Element of P} c= P by TARSKI:def 1, B3;
then B2: P = (P \ { the Element of P}) \/ { the Element of P} by FIELD_5:1;
then card P = (card (P \ { the Element of P})) + 1 by B1, CARD_2:41;
then consider K being FieldExtension of F such that
C: for p being non constant Element of the carrier of (Polynom-Ring F) st p in P \ { the Element of P} holds
p is_with_roots_in K by A, AS;
reconsider p = the Element of P as Element of the carrier of (Polynom-Ring F) by B3;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring K) by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of (Polynom-Ring K) ;

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

suppose E0: p1 is constant ; :: thesis: ex E being FieldExtension of E st
for p being non constant Element of the carrier of (Polynom-Ring E) st b₄ in p holds
b₄ is_with_roots_in b₃

now :: thesis: for q being non constant Element of the carrier of (Polynom-Ring F) st q in P holds
q is_with_roots_in K

let q be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( q in P implies q is_with_roots_in K )
H: deg q > 0 by RING_4:def 4;
assume E1: q in P ; :: thesis: q is_with_roots_in K
q <> p by H, E0, FIELD_4:20;
then not q in {p} by TARSKI:def 1;
then q in P \ { the Element of P} by B2, E1, XBOOLE_0:def 3;
hence q is_with_roots_in K by C; :: thesis: verum

end;

hence ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E ; :: thesis: verum

end;

suppose not p1 is constant ; :: thesis: ex E being FieldExtension of E st
for p being non constant Element of the carrier of (Polynom-Ring E) st b₄ in p holds
b₄ is_with_roots_in b₃

then reconsider p1 = p1 as non constant Element of the carrier of (Polynom-Ring K) ;
consider E being FieldExtension of K such that
D: p1 is_with_roots_in E by FIELD_5:30;
E: K is Subring of E by FIELD_4:def 1;
reconsider E = E as K -extending FieldExtension of F ;

now :: thesis: for q being non constant Element of the carrier of (Polynom-Ring F) st q in P holds
q is_with_roots_in E

let q be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( q in P implies b₁ is_with_roots_in E )
assume E1: q in P ; :: thesis: b₁ is_with_roots_in E

per cases ( q = p1 or q <> p1 ) ;

suppose E2: q = p1 ; :: thesis: b₁ is_with_roots_in E

consider a being Element of E such that
E3: a is_a_root_of p1,E by D, FIELD_4:def 3;
E4: Ext_eval (p1,a) = 0. E by E3, FIELD_4:def 2;
Ext_eval (p1,a) = Ext_eval (p,a) by FIELD_7:15;
hence q is_with_roots_in E by E2, E4, FIELD_4:def 2, FIELD_4:def 3; :: thesis: verum

end;

suppose q <> p1 ; :: thesis: b₁ is_with_roots_in E

then not q in {p} by TARSKI:def 1;
then q in P \ { the Element of P} by E1, B2, XBOOLE_0:def 3;
then consider a being Element of K such that
E3: a is_a_root_of q,K by C, FIELD_4:def 3;
the carrier of K c= the carrier of E by E, C0SP1:def 3;
then reconsider a1 = a as Element of E ;
Ext_eval (q,a1) = Ext_eval (q,a) by FIELD_7:14
.= 0. K by E3, FIELD_4:def 2
.= 0. E by E, C0SP1:def 3 ;
hence q is_with_roots_in E by FIELD_4:def 2, FIELD_4:def 3; :: thesis: verum

end;

end;

end;

hence ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E ; :: thesis: verum

end;

end;

end;

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

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
consider n being Nat such that
H: card P = n ;
thus ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E by I, H; :: thesis: verum