set FX = Polynom-Ring F;
set I = {p} -Ideal ;
set K = (Polynom-Ring F) / ({p} -Ideal);
set x = the Element of ([#] ((Polynom-Ring F) / ({p} -Ideal))) /\ ([#] (Polynom-Ring ((Polynom-Ring F) / ({p} -Ideal))));

now :: thesis: (Polynom-Ring F) / ({p} -Ideal) is polynomial_disjoint

assume A1: not (Polynom-Ring F) / ({p} -Ideal) is polynomial_disjoint ; :: thesis: contradiction
then A2: ( the Element of ([#] ((Polynom-Ring F) / ({p} -Ideal))) /\ ([#] (Polynom-Ring ((Polynom-Ring F) / ({p} -Ideal)))) in [#] ((Polynom-Ring F) / ({p} -Ideal)) & the Element of ([#] ((Polynom-Ring F) / ({p} -Ideal))) /\ ([#] (Polynom-Ring ((Polynom-Ring F) / ({p} -Ideal)))) in [#] (Polynom-Ring ((Polynom-Ring F) / ({p} -Ideal))) ) by XBOOLE_0:def 4;
reconsider x = the Element of ([#] ((Polynom-Ring F) / ({p} -Ideal))) /\ ([#] (Polynom-Ring ((Polynom-Ring F) / ({p} -Ideal)))) as Element of ((Polynom-Ring F) / ({p} -Ideal)) by A1, XBOOLE_0:def 4;
reconsider q = x as Polynomial of ((Polynom-Ring F) / ({p} -Ideal)) by A2, POLYNOM3:def 10;
consider a being Element of (Polynom-Ring F) such that
A3: x = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),a) by RING_1:11;
reconsider p = a as Polynomial of F by POLYNOM3:def 10;
for o being object st o in q holds
ex n being Element of NAT ex u being object st o = [n,u]

proof

let o be object ; :: thesis: ( o in q implies ex n being Element of NAT ex u being object st o = [n,u] )
assume o in q ; :: thesis: ex n being Element of NAT ex u being object st o = [n,u]
then consider a, b being object such that
A4: ( a in NAT & b in [#] ((Polynom-Ring F) / ({p} -Ideal)) & o = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a as Element of NAT by A4;
take a ; :: thesis: ex u being object st o = [a,u]
take b ; :: thesis: o = [a,b]
thus o = [a,b] by A4; :: thesis: verum

end;

then consider n being Element of NAT , u being object such that
A5: p = [n,u] by A3, EQREL_1:20;
dom p = NAT by FUNCT_2:def 1;
then [n,(p . n)] in p by FUNCT_1:1;
then A6: [n,(p . n)] in {{n},{n,u}} by A5, TARSKI:def 5;

now :: thesis: for a, b being object holds not [n,a] in {{n},{n,b}}

let a, b be object ; :: thesis: not [n,a] in {{n},{n,b}}
assume [n,a] in {{n},{n,b}} ; :: thesis: contradiction
then A7: {{n},{n,a}} in {{n},{n,b}} by TARSKI:def 5;

per cases ( {{n},{n,a}} = {n} or {{n},{n,a}} = {n,b} ) by A7, TARSKI:def 2;

suppose A8: {{n},{n,a}} = {n} ; :: thesis: contradiction

{n} in {{n},{n,a}} by TARSKI:def 2;
hence contradiction by A8; :: thesis: verum

end;

suppose A9: {{n},{n,a}} = {n,b} ; :: thesis: contradiction

A10: n in {n,b} by TARSKI:def 2;

per cases ( n = {n} or n = {n,a} ) by A10, A9, TARSKI:def 2;

suppose n = {n} ; :: thesis: contradiction

then n in n by TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

suppose n = {n,a} ; :: thesis: contradiction

then n in n by TARSKI:def 2;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

end;

hence contradiction by A6; :: thesis: verum

end;

hence (Polynom-Ring F) / ({p} -Ideal) is polynomial_disjoint ; :: thesis: verum