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

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 )

hence
F, Polynom-Ring p are_disjoint
; :: thesis: verumassume
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;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