deffunc H1( object ) -> Element of bool the carrier of () = Class ((EqRel ((),())),\$1);
A1: the carrier of () = { 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 () holds
H1(x) in the carrier of (KroneckerField (F,p))
let x be object ; :: thesis: ( x in the carrier of () implies H1(x) in the carrier of (KroneckerField (F,p)) )
assume A3: x in the carrier of () ; :: thesis: H1(x) in the carrier of (KroneckerField (F,p))
for a being Element of () holds a in the carrier of ()
proof
let a be Element of (); :: thesis: a in the carrier of ()
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 () by POLYNOM3:def 10; :: thesis: verum
end;
then reconsider a = x as Element of () by A3;
Class ((EqRel ((),())),a) is Element of (() / ()) by RING_1:12;
then Class ((EqRel ((),())),a) in the carrier of (() / ()) ;
hence H1(x) in the carrier of (KroneckerField (F,p)) by FIELD_1:def 3; :: thesis: verum
end;
consider g being Function of the carrier of (), the carrier of (KroneckerField (F,p)) such that
A4: for x being object st x in the carrier of () holds
g . x = H1(x) from take g ; :: thesis: for q being Element of the carrier of () holds g . q = Class ((EqRel ((),())),q)
thus for q being Element of the carrier of () holds g . q = Class ((EqRel ((),())),q) by A4; :: thesis: verum