let F be polynomial_disjoint Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds F, Polynom-Ring p are_disjoint
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: F, Polynom-Ring p are_disjoint

now :: thesis: ( not F, Polynom-Ring p are_disjoint implies for a being Element of the carrier of F /\ the carrier of (Polynom-Ring p) holds contradiction )

assume not F, Polynom-Ring p are_disjoint ; :: thesis: for a being Element of the carrier of F /\ the carrier of (Polynom-Ring p) holds contradiction
then A: ([#] F) /\ ([#] (Polynom-Ring p)) <> {} by FIELD_2:def 1;
let a be Element of the carrier of F /\ the carrier of (Polynom-Ring p); :: thesis: contradiction
B: ( a in the carrier of F & a in the carrier of (Polynom-Ring p) ) by A, XBOOLE_0:def 4;
the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;
then consider q being Polynomial of F such that
C: ( a = q & deg q < deg p ) by B;
a in the carrier of (Polynom-Ring F) by C, POLYNOM3:def 10;
then a in ([#] F) /\ ([#] (Polynom-Ring F)) by B, XBOOLE_0:def 4;
hence contradiction by FIELD_3:def 3; :: thesis: verum

end;

hence F, Polynom-Ring p are_disjoint ; :: thesis: verum