deffunc H_{1}( 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;

A4: for x being object st x in the carrier of (Polynom-Ring p) holds

g . x = H_{1}(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

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_{1}(x) in the carrier of (KroneckerField (F,p))

consider g being Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) such that H

let x be object ; :: thesis: ( x in the carrier of (Polynom-Ring p) implies H_{1}(x) in the carrier of (KroneckerField (F,p)) )

assume A3: x in the carrier of (Polynom-Ring p) ; :: thesis: H_{1}(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)

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_{1}(x) in the carrier of (KroneckerField (F,p))
by FIELD_1:def 3; :: thesis: verum

end;assume A3: x in the carrier of (Polynom-Ring p) ; :: thesis: H

for a being Element of (Polynom-Ring p) holds a in the carrier of (Polynom-Ring F)

proof

then reconsider a = x as Element of (Polynom-Ring F) by A3;
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;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

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

A4: for x being object st x in the carrier of (Polynom-Ring p) holds

g . x = H

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