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

now :: thesis:

assume not embField (emb p) is polynomial_disjoint ; :: thesis:
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;
Z/ n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #) by INT_3:def 12;
then not q in the carrier of (Z/ n) by FIELD_3:24;
then the Element of the carrier of (embField (emb p)) /\ the carrier of (Polynom-Ring (embField (emb p))) in the carrier of (KroneckerField ((Z/ n),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 (Z/ n)) / ({p} -Ideal)) ;
consider a being Element of (Polynom-Ring (Z/ n)) such that
B: o = Class ((EqRel ((Polynom-Ring (Z/ n)),({p} -Ideal))),a) by RING_1:11;
reconsider q = q as Polynomial of (embField (emb p)) ;
a - a = 0. (Polynom-Ring (Z/ n)) 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 (Z/ n) 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:

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

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

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

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:

end;

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

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

per cases by F1, TARSKI:def 2;

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

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

end;

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

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

end;

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

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

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:

end;

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

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 ;

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

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

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

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:

end;

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

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

per cases by F1, TARSKI:def 2;

suppose i = {2} ; :: thesis:

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

end;

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

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:

end;

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

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

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

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

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:

end;

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

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

per cases by F1, TARSKI:def 2;

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

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

end;

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

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

end;

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