let F be Field; for p being Element of the carrier of (Polynom-Ring F) holds { q where q is Polynomial of F : deg q < deg p } is Preserv of the addF of (Polynom-Ring F)
let p be Element of the carrier of (Polynom-Ring F); { q where q is Polynomial of F : deg q < deg p } is Preserv of the addF of (Polynom-Ring F)
set C = { q where q is Polynomial of F : deg q < deg p } ;
then
{ q where q is Polynomial of F : deg q < deg p } c= the carrier of (Polynom-Ring F)
;
then reconsider C = { q where q is Polynomial of F : deg q < deg p } as Subset of the carrier of (Polynom-Ring F) ;
set A = the addF of (Polynom-Ring F);
now for x being set st x in [:C,C:] holds
the addF of (Polynom-Ring F) . x in Clet x be
set ;
( x in [:C,C:] implies the addF of (Polynom-Ring F) . x in C )assume
x in [:C,C:]
;
the addF of (Polynom-Ring F) . x in Cthen consider a,
b being
object such that A2:
a in C
and A3:
b in C
and A4:
x = [a,b]
by ZFMISC_1:def 2;
consider u being
Polynomial of
F such that A5:
(
a = u &
deg u < deg p )
by A2;
consider v being
Polynomial of
F such that A6:
(
b = v &
deg v < deg p )
by A3;
reconsider a =
a,
b =
b as
Element of
(Polynom-Ring F) by A5, A6, POLYNOM3:def 10;
A7:
deg (u + v) <= max (
(deg u),
(deg v))
by HURWITZ:22;
max (
(deg u),
(deg v))
< deg p
by A5, A6, XXREAL_0:29;
then A8:
deg (u + v) < deg p
by A7, XXREAL_0:2;
the
addF of
(Polynom-Ring F) . x =
a + b
by A4
.=
u + v
by A5, A6, POLYNOM3:def 10
;
hence
the
addF of
(Polynom-Ring F) . x in C
by A8;
verum end;
hence
{ q where q is Polynomial of F : deg q < deg p } is Preserv of the addF of (Polynom-Ring F)
by REALSET1:def 1; verum