A1: the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;

now :: thesis: for o being object st o in the carrier of (Polynom-Ring p) holds
o is Polynomial of F

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring p) implies o is Polynomial of F )
assume o in the carrier of (Polynom-Ring p) ; :: thesis: o is Polynomial of F
then consider q being Polynomial of F such that
A2: ( q = o & deg q < deg p ) by A1;
thus o is Polynomial of F by A2; :: thesis: verum

end;

hence the carrier of (Polynom-Ring p) is F -polynomial-membered ; :: thesis: verum