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;

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

hence
Polynom-Ring p is polynomial_disjoint
; :: thesis: verumassume
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;

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)

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;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)

then
rng r c= [#] (Polynom-Ring F)
;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;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

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

then
y is finite-Support
by ALGSEQ_1:def 1;
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)

y . i = 0. (Polynom-Ring F) ; :: thesis: verum

end;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)

hence
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;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

y . i = 0. (Polynom-Ring F) ; :: thesis: verum

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