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 ;

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

hence
embField (emb p) is polynomial_disjoint
; :: thesis: verumassume
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;

end;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

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

end;

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;{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

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;

end;i in {i,(q . i)} by TARSKI:def 2;

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

end;

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;( {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

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;

end;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 )
;

end;

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

end;

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

end;

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;{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

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;

end;i in {i,(q . i)} by TARSKI:def 2;

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

end;

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;2 in {2} by TARSKI:def 1;

hence contradiction by F3, TARSKI:def 1; :: thesis: verum

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;2 in {2,(a . 2)} by TARSKI:def 2;

hence contradiction by F3, TARSKI:def 1; :: thesis: verum

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

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

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

end;

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;( {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

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;

end;2 in {2,(q . i)} by TARSKI:def 2;