set E = KroneckerField (F,p);
reconsider q = <%(0. F),(1. F)%> as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) is Element of (KroneckerField (F,p)) by RING_1:12;
hence Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),<%(0. F),(1. F)%>) is Element of (KroneckerField (F,p)) ; :: thesis: verum