let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds { q where q is Polynomial of F : deg q < deg p } is Preserv of poly_mult_mod p
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: { q where q is Polynomial of F : deg q < deg p } is Preserv of poly_mult_mod p
set C = { q where q is Polynomial of F : deg q < deg p } ;

now :: thesis: for x being set st x in { q where q is Polynomial of F : deg q < deg p } holds
x in the carrier of (Polynom-Ring F)

let x be set ; :: thesis: ( x in { q where q is Polynomial of F : deg q < deg p } implies x in the carrier of (Polynom-Ring F) )
assume x in { q where q is Polynomial of F : deg q < deg p } ; :: thesis: x in the carrier of (Polynom-Ring F)
then ex r being Polynomial of F st
( x = r & deg r < deg p ) ;
hence x in the carrier of (Polynom-Ring F) by POLYNOM3:def 10; :: thesis: verum

end;

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 = poly_mult_mod p;

now :: thesis: for x being set st x in [:C,C:] holds
(poly_mult_mod p) . x in C

let x be set ; :: thesis: ( x in [:C,C:] implies (poly_mult_mod p) . x in C )
assume x in [:C,C:] ; :: thesis: (poly_mult_mod p) . x in C
then 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;
A8: deg ((u *' v) mod p) < deg p by RING_2:29;
(poly_mult_mod p) . x = (poly_mult_mod p) . (u,v) by A5, A6, A4
.= (u *' v) mod p by defpmm ;
hence (poly_mult_mod p) . x in C by A8; :: thesis: verum

end;

hence { q where q is Polynomial of F : deg q < deg p } is Preserv of poly_mult_mod p by REALSET1:def 1; :: thesis: verum