set RX = Polynom-Ring p;
set FX = Polynom-Ring F;
set M = ([#] ()) /\ ([#] ());
set x = the Element of ([#] ()) /\ ([#] ());
A1: [#] () = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;
now :: thesis:
assume not Polynom-Ring p is polynomial_disjoint ; :: thesis: contradiction
then A2: ( the Element of ([#] ()) /\ ([#] ()) in [#] () & the Element of ([#] ()) /\ ([#] ()) in [#] () ) by XBOOLE_0:def 4;
then consider q being Polynomial of F such that
A3: ( the Element of ([#] ()) /\ ([#] ()) = q & deg q < deg p ) by A1;
reconsider r = the Element of ([#] ()) /\ ([#] ()) as Polynomial of () by ;
now :: thesis: for o being object st o in rng r holds
o in [#] ()
let o be object ; :: thesis: ( o in rng r implies o in [#] () )
assume A4: o in rng r ; :: thesis: o in [#] ()
rng r c= [#] () by RELAT_1:def 19;
then o in [#] () by A4;
then consider u being Polynomial of F such that
A5: ( o = u & deg u < deg p ) by A1;
thus o in [#] () by ; :: thesis: verum
end;
then rng r c= [#] () ;
then reconsider y = the Element of ([#] ()) /\ ([#] ()) as Function of NAT,() by FUNCT_2:6;
ex n being Nat st
for i being Nat st i >= n holds
y . i = 0. ()
proof
consider n being Nat such that
A6: for i being Nat st i >= n holds
r . i = 0. () by ALGSEQ_1:def 1;
take n ; :: thesis: for i being Nat st i >= n holds
y . i = 0. ()

now :: thesis: for i being Nat st i >= n holds
y . i = 0. ()
let i be Nat; :: thesis: ( i >= n implies y . i = 0. () )
assume i >= n ; :: thesis: y . i = 0. ()
hence y . i = 0. () by A6
.= 0_. F by RING_4:def 8
.= 0. () by POLYNOM3:def 10 ;
:: thesis: verum
end;
hence for i being Nat st i >= n holds
y . i = 0. () ; :: thesis: verum
end;
then y is finite-Support by ALGSEQ_1:def 1;
then A8: the Element of ([#] ()) /\ ([#] ()) in [#] () by POLYNOM3:def 10;
the Element of ([#] ()) /\ ([#] ()) in [#] () by ;
then the Element of ([#] ()) /\ ([#] ()) in ([#] ()) /\ ([#] ()) by ;
hence contradiction by Def3; :: thesis: verum
end;
hence Polynom-Ring p is polynomial_disjoint ; :: thesis: verum