let F be Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F)

for E being polynomial_disjoint Field st E = embField (emb p) holds

F is polynomial_disjoint

let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for E being polynomial_disjoint Field st E = embField (emb p) holds

F is polynomial_disjoint

let E be polynomial_disjoint Field; :: thesis: ( E = embField (emb p) implies F is polynomial_disjoint )

assume AS1: E = embField (emb p) ; :: thesis: F is polynomial_disjoint

assume AS2: not F is polynomial_disjoint ; :: thesis: contradiction

H: F is Subfield of E by AS1, FIELD_2:17;

then reconsider K = E as FieldExtension of F by FIELD_4:7;

A: the carrier of F c= the carrier of K by H, EC_PF_1:def 1;

set o = the Element of the carrier of F /\ the carrier of (Polynom-Ring F);

([#] F) /\ ([#] (Polynom-Ring F)) <> {} by AS2, FIELD_3:def 3;

then B: ( the Element of the carrier of F /\ the carrier of (Polynom-Ring F) in the carrier of F & the Element of the carrier of F /\ the carrier of (Polynom-Ring F) in the carrier of (Polynom-Ring F) ) by XBOOLE_0:def 4;

the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring K) by FIELD_4:10;

then the Element of the carrier of F /\ the carrier of (Polynom-Ring F) in ([#] K) /\ ([#] (Polynom-Ring K)) by A, B, XBOOLE_0:def 4;

hence contradiction by FIELD_3:def 3; :: thesis: verum

for E being polynomial_disjoint Field st E = embField (emb p) holds

F is polynomial_disjoint

let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for E being polynomial_disjoint Field st E = embField (emb p) holds

F is polynomial_disjoint

let E be polynomial_disjoint Field; :: thesis: ( E = embField (emb p) implies F is polynomial_disjoint )

assume AS1: E = embField (emb p) ; :: thesis: F is polynomial_disjoint

assume AS2: not F is polynomial_disjoint ; :: thesis: contradiction

H: F is Subfield of E by AS1, FIELD_2:17;

then reconsider K = E as FieldExtension of F by FIELD_4:7;

A: the carrier of F c= the carrier of K by H, EC_PF_1:def 1;

set o = the Element of the carrier of F /\ the carrier of (Polynom-Ring F);

([#] F) /\ ([#] (Polynom-Ring F)) <> {} by AS2, FIELD_3:def 3;

then B: ( the Element of the carrier of F /\ the carrier of (Polynom-Ring F) in the carrier of F & the Element of the carrier of F /\ the carrier of (Polynom-Ring F) in the carrier of (Polynom-Ring F) ) by XBOOLE_0:def 4;

the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring K) by FIELD_4:10;

then the Element of the carrier of F /\ the carrier of (Polynom-Ring F) in ([#] K) /\ ([#] (Polynom-Ring K)) by A, B, XBOOLE_0:def 4;

hence contradiction by FIELD_3:def 3; :: thesis: verum