Poly (m,<%(0. F),(1. F)%>) is Element of (Polynom-Ring ((card (nonConstantPolys F)),F)) by POLYNOM1:def 11;
hence Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,<%(0. F),(1. F)%>))) is Element of (KroneckerField (F,g,I)) by RING_1:12; :: thesis: verum