deffunc H₁( object ) -> Element of bool the carrier of (Polynom-Ring F) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),$1);
A1: the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;

A2: now :: thesis: for x being object st x in the carrier of (Polynom-Ring p) holds
H₁(x) in the carrier of (KroneckerField (F,p))

let x be object ; :: thesis: ( x in the carrier of (Polynom-Ring p) implies H₁(x) in the carrier of (KroneckerField (F,p)) )
assume A3: x in the carrier of (Polynom-Ring p) ; :: thesis: H₁(x) in the carrier of (KroneckerField (F,p))
for a being Element of (Polynom-Ring p) holds a in the carrier of (Polynom-Ring F)

proof

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

end;

then reconsider a = x as Element of (Polynom-Ring F) by A3;
Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),a) is Element of ((Polynom-Ring F) / ({p} -Ideal)) by RING_1:12;
then Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),a) in the carrier of ((Polynom-Ring F) / ({p} -Ideal)) ;
hence H₁(x) in the carrier of (KroneckerField (F,p)) by FIELD_1:def 3; :: thesis: verum

end;

consider g being Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) such that
A4: for x being object st x in the carrier of (Polynom-Ring p) holds
g . x = H₁(x) from FUNCT_2:sch 2(A2);
take g ; :: thesis: for q being Element of the carrier of (Polynom-Ring p) holds g . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q)
thus for q being Element of the carrier of (Polynom-Ring p) holds g . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) by A4; :: thesis: verum