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

hence
the carrier of (Polynom-Ring p) is F -polynomial-membered
; :: thesis: verumo 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;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