set RX = Polynom-Ring p;
set FX = Polynom-Ring F;
set M = ([#] (Polynom-Ring p)) /\ ([#] (Polynom-Ring (Polynom-Ring p)));
set x = the Element of ([#] (Polynom-Ring p)) /\ ([#] (Polynom-Ring (Polynom-Ring p)));
A1: [#] (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;

now :: thesis: Polynom-Ring p is polynomial_disjoint

assume not Polynom-Ring p is polynomial_disjoint ; :: thesis: contradiction
then A2: ( the Element of ([#] (Polynom-Ring p)) /\ ([#] (Polynom-Ring (Polynom-Ring p))) in [#] (Polynom-Ring p) & the Element of ([#] (Polynom-Ring p)) /\ ([#] (Polynom-Ring (Polynom-Ring p))) in [#] (Polynom-Ring (Polynom-Ring p)) ) by XBOOLE_0:def 4;
then consider q being Polynomial of F such that
A3: ( the Element of ([#] (Polynom-Ring p)) /\ ([#] (Polynom-Ring (Polynom-Ring p))) = q & deg q < deg p ) by A1;
reconsider r = the Element of ([#] (Polynom-Ring p)) /\ ([#] (Polynom-Ring (Polynom-Ring p))) as Polynomial of (Polynom-Ring p) by A2, POLYNOM3:def 10;

now :: thesis: for o being object st o in rng r holds
o in [#] (Polynom-Ring F)

let o be object ; :: thesis: ( o in rng r implies o in [#] (Polynom-Ring F) )
assume A4: o in rng r ; :: thesis: o in [#] (Polynom-Ring F)
rng r c= [#] (Polynom-Ring p) by RELAT_1:def 19;
then o in [#] (Polynom-Ring p) by A4;
then consider u being Polynomial of F such that
A5: ( o = u & deg u < deg p ) by A1;
thus o in [#] (Polynom-Ring F) by A5, POLYNOM3:def 10; :: thesis: verum

end;

then rng r c= [#] (Polynom-Ring F) ;
then reconsider y = the Element of ([#] (Polynom-Ring p)) /\ ([#] (Polynom-Ring (Polynom-Ring p))) as Function of NAT,(Polynom-Ring F) by FUNCT_2:6;
ex n being Nat st
for i being Nat st i >= n holds
y . i = 0. (Polynom-Ring F)

proof

consider n being Nat such that
A6: for i being Nat st i >= n holds
r . i = 0. (Polynom-Ring p) by ALGSEQ_1:def 1;
take n ; :: thesis: for i being Nat st i >= n holds
y . i = 0. (Polynom-Ring F)

now :: thesis: for i being Nat st i >= n holds
y . i = 0. (Polynom-Ring F)

let i be Nat; :: thesis: ( i >= n implies y . i = 0. (Polynom-Ring F) )
assume i >= n ; :: thesis: y . i = 0. (Polynom-Ring F)
hence y . i = 0. (Polynom-Ring p) by A6
.= 0_. F by RING_4:def 8
.= 0. (Polynom-Ring F) by POLYNOM3:def 10 ;
:: thesis: verum

end;

hence for i being Nat st i >= n holds
y . i = 0. (Polynom-Ring F) ; :: thesis: verum

end;

then y is finite-Support by ALGSEQ_1:def 1;
then A8: the Element of ([#] (Polynom-Ring p)) /\ ([#] (Polynom-Ring (Polynom-Ring p))) in [#] (Polynom-Ring (Polynom-Ring F)) by POLYNOM3:def 10;
the Element of ([#] (Polynom-Ring p)) /\ ([#] (Polynom-Ring (Polynom-Ring p))) in [#] (Polynom-Ring F) by A3, POLYNOM3:def 10;
then the Element of ([#] (Polynom-Ring p)) /\ ([#] (Polynom-Ring (Polynom-Ring p))) in ([#] (Polynom-Ring F)) /\ ([#] (Polynom-Ring (Polynom-Ring F))) by A8, XBOOLE_0:def 4;
hence contradiction by Def3; :: thesis: verum

end;

hence Polynom-Ring p is polynomial_disjoint ; :: thesis: verum