set F = embField (emb p);
set FX = Polynom-Ring (embField (emb p));
set f = emb p;
set Kr = KroneckerField (F_Rat,p);
set o = the Element of the carrier of (embField (emb p)) /\ the carrier of (Polynom-Ring (embField (emb p)));
X: ( [#] F_Rat = the carrier of F_Rat & [#] (KroneckerField (F_Rat,p)) = the carrier of (KroneckerField (F_Rat,p)) ) ;
H: the carrier of (embField (emb p)) = carr (emb p) by FIELD_2:def 7
.= ( the carrier of (KroneckerField (F_Rat,p)) \ (rng (emb p))) \/ the carrier of F_Rat by X, FIELD_2:def 2 ;

now :: thesis: embField (emb p) is polynomial_disjoint

assume not embField (emb p) is polynomial_disjoint ; :: thesis: contradiction
then A1: ([#] (embField (emb p))) /\ ([#] (Polynom-Ring (embField (emb p)))) <> {} by FIELD_3:def 3;
then A: ( the Element of the carrier of (embField (emb p)) /\ the carrier of (Polynom-Ring (embField (emb p))) in the carrier of (embField (emb p)) & the Element of the carrier of (embField (emb p)) /\ the carrier of (Polynom-Ring (embField (emb p))) in the carrier of (Polynom-Ring (embField (emb p))) ) by XBOOLE_0:def 4;
reconsider q = the Element of the carrier of (embField (emb p)) /\ the carrier of (Polynom-Ring (embField (emb p))) as Element of the carrier of (Polynom-Ring (embField (emb p))) by A1, XBOOLE_0:def 4;
not q in the carrier of F_Rat by FIELD_3:25;
then the Element of the carrier of (embField (emb p)) /\ the carrier of (Polynom-Ring (embField (emb p))) in the carrier of (KroneckerField (F_Rat,p)) \ (rng (emb p)) by H, A, XBOOLE_0:def 3;
then reconsider o = the Element of the carrier of (embField (emb p)) /\ the carrier of (Polynom-Ring (embField (emb p))) as Element of ((Polynom-Ring F_Rat) / ({p} -Ideal)) ;
consider a being Element of (Polynom-Ring F_Rat) such that
B: o = Class ((EqRel ((Polynom-Ring F_Rat),({p} -Ideal))),a) by RING_1:11;
reconsider q = q as Polynomial of (embField (emb p)) ;
a - a = 0. (Polynom-Ring F_Rat) by RLVECT_1:15;
then D0: a in q by B, RING_1:5, IDEAL_1:3;
then consider i, z being object such that
D1: ( i in NAT & z in the carrier of (embField (emb p)) & a = [i,z] ) by ZFMISC_1:def 2;
D2: z = q . i by D0, D1, FUNCT_1:1;
reconsider i = i as Element of NAT by D1;
reconsider a = a as Polynomial of F_Rat by POLYNOM3:def 10;
dom a = NAT by FUNCT_2:def 1;
then ( [1,(a . 1)] in a & [2,(a . 2)] in a ) by FUNCT_1:1;
then E: ( [1,(a . 1)] in {{i},{i,(q . i)}} & [2,(a . 2)] in {{i},{i,(q . i)}} ) by D1, D2, TARSKI:def 5;

F: now :: thesis: not i = {1}

assume E3: i = {1} ; :: thesis: contradiction

per cases ( [2,(a . 2)] = {i} or [2,(a . 2)] = {i,(q . i)} ) by E, TARSKI:def 2;

suppose [2,(a . 2)] = {i} ; :: thesis: contradiction

then F1: {i} = {{2},{2,(a . 2)}} by TARSKI:def 5;
{2} in {{2},{2,(a . 2)}} by TARSKI:def 2;
then F3: {2} = {1} by E3, F1, TARSKI:def 1;
2 in {2} by TARSKI:def 1;
hence contradiction by F3, TARSKI:def 1; :: thesis: verum

end;

suppose [2,(a . 2)] = {i,(q . i)} ; :: thesis: contradiction

then F1: {i,(q . i)} = {{2},{2,(a . 2)}} by TARSKI:def 5;
i in {i,(q . i)} by TARSKI:def 2;

per cases then ( i = {2} or i = {2,(a . 2)} ) by F1, TARSKI:def 2;

suppose F3: i = {2} ; :: thesis: contradiction

2 in {2} by TARSKI:def 1;
hence contradiction by E3, F3, TARSKI:def 1; :: thesis: verum

end;

suppose F3: i = {2,(a . 2)} ; :: thesis: contradiction

2 in {2,(a . 2)} by TARSKI:def 2;
hence contradiction by E3, F3, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

end;

per cases ( [1,(a . 1)] = {i} or [1,(a . 1)] = {i,(q . i)} ) by E, TARSKI:def 2;

suppose [1,(a . 1)] = {i} ; :: thesis: contradiction

then E1: {i} = {{1},{1,(a . 1)}} by TARSKI:def 5;
( {1} in {{1},{1,(a . 1)}} & {1,(a . 1)} in {{1},{1,(a . 1)}} ) by TARSKI:def 2;
hence contradiction by F, E1, TARSKI:def 1; :: thesis: verum

end;

suppose [1,(a . 1)] = {i,(q . i)} ; :: thesis: contradiction

then E1: {i,(q . i)} = {{1},{1,(a . 1)}} by TARSKI:def 5;
i in {i,(q . i)} by TARSKI:def 2;
then F0: i = {1,(a . 1)} by F, E1, TARSKI:def 2;

per cases ( 1 = a . 1 or 1 <> a . 1 ) ;

suppose E3: 1 = a . 1 ; :: thesis: contradiction

per cases ( [2,(a . 2)] = {i} or [2,(a . 2)] = {i,(q . i)} ) by E, TARSKI:def 2;

suppose [2,(a . 2)] = {i} ; :: thesis: contradiction

then F1: {i} = {{2},{2,(a . 2)}} by TARSKI:def 5;
{2} in {{2},{2,(a . 2)}} by TARSKI:def 2;
then F3: {2} = i by F1, TARSKI:def 1
.= {1} by E3, F0, ENUMSET1:29 ;
2 in {2} by TARSKI:def 1;
hence contradiction by F3, TARSKI:def 1; :: thesis: verum

end;

suppose [2,(a . 2)] = {i,(q . i)} ; :: thesis: contradiction

then F1: {i,(q . i)} = {{2},{2,(a . 2)}} by TARSKI:def 5;
i in {i,(q . i)} by TARSKI:def 2;

per cases then ( i = {2} or i = {2,(a . 2)} ) by F1, TARSKI:def 2;

suppose i = {2} ; :: thesis: contradiction

then F3: {2} = {1} by E3, F0, ENUMSET1:29;
2 in {2} by TARSKI:def 1;
hence contradiction by F3, TARSKI:def 1; :: thesis: verum

end;

suppose i = {2,(a . 2)} ; :: thesis: contradiction

then F3: {1} = {2,(a . 2)} by E3, F0, ENUMSET1:29;
2 in {2,(a . 2)} by TARSKI:def 2;
hence contradiction by F3, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

end;

suppose 1 <> a . 1 ; :: thesis: contradiction

then G1: a . 1 = 0 by F0, FIELD_3:2;

per cases ( [2,(a . 2)] = {i} or [2,(a . 2)] = {i,(q . i)} ) by E, TARSKI:def 2;

suppose [2,(a . 2)] = {i} ; :: thesis: contradiction

then F1: {{1,(a . 1)}} = {{2},{2,(a . 2)}} by F0, TARSKI:def 5;
( {2} in {{2},{2,(a . 2)}} & {2,(a . 2)} in {{2},{2,(a . 2)}} ) by TARSKI:def 2;
hence contradiction by G1, F1, CARD_1:50; :: thesis: verum

end;

suppose [2,(a . 2)] = {i,(q . i)} ; :: thesis: contradiction

then F1: {2,(q . i)} = {{2},{2,(a . 2)}} by CARD_1:50, F0, G1, TARSKI:def 5;
2 in {2,(q . i)} by TARSKI:def 2;

per cases then ( 2 = {2} or 2 = {2,(a . 2)} ) by F1, TARSKI:def 2;

suppose F2: 2 = {2} ; :: thesis: contradiction

2 in {2} by TARSKI:def 1;
hence contradiction by F2; :: thesis: verum

end;

suppose F2: 2 = {2,(a . 2)} ; :: thesis: contradiction

2 in {2,(a . 2)} by TARSKI:def 2;
hence contradiction by F2; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

hence embField (emb p) is polynomial_disjoint ; :: thesis: verum