let F be Field; :: thesis: for p being linear Element of the carrier of (Polynom-Ring F) holds

( (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic & the carrier of (embField (emb p)) = the carrier of F )

let p be linear Element of the carrier of (Polynom-Ring F); :: thesis: ( (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic & the carrier of (embField (emb p)) = the carrier of F )

set FP = (Polynom-Ring F) / ({p} -Ideal);

set I = {p} -Ideal ;

set f = emb p;

set FX = Polynom-Ring F;

A: (Polynom-Ring F) / ({p} -Ideal), Polynom-Ring p are_isomorphic by RING_4:48;

Polynom-Ring p,F are_isomorphic by polyd;

hence (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic by A, RING_3:44; :: thesis: the carrier of (embField (emb p)) = the carrier of F

X: ( [#] F = the carrier of F & [#] ((Polynom-Ring F) / ({p} -Ideal)) = the carrier of ((Polynom-Ring F) / ({p} -Ideal)) ) ;

thus the carrier of (embField (emb p)) = carr (emb p) by FIELD_2:def 7

.= ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the carrier of F by X, FIELD_2:def 2

.= {} \/ the carrier of F by C, XBOOLE_1:37

.= the carrier of F ; :: thesis: verum

( (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic & the carrier of (embField (emb p)) = the carrier of F )

let p be linear Element of the carrier of (Polynom-Ring F); :: thesis: ( (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic & the carrier of (embField (emb p)) = the carrier of F )

set FP = (Polynom-Ring F) / ({p} -Ideal);

set I = {p} -Ideal ;

set f = emb p;

set FX = Polynom-Ring F;

A: (Polynom-Ring F) / ({p} -Ideal), Polynom-Ring p are_isomorphic by RING_4:48;

Polynom-Ring p,F are_isomorphic by polyd;

hence (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic by A, RING_3:44; :: thesis: the carrier of (embField (emb p)) = the carrier of F

B: now :: thesis: for q being Element of the carrier of (Polynom-Ring F) ex r being constant Element of the carrier of (Polynom-Ring F) st Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),r)

let q be Element of the carrier of (Polynom-Ring F); :: thesis: ex r being constant Element of the carrier of (Polynom-Ring F) st Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),r)

B1: q = ((q div p) *' p) + (q mod p) by RING_4:4;

reconsider r = q mod p, d = q div p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

deg r < deg p by divmod;

then deg r < 1 by defl;

then (deg r) + 1 <= 1 by INT_1:7;

then ((deg r) + 1) - 1 <= 1 - 1 by XREAL_1:9;

then reconsider r = r as constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4;

(q div p) *' p = d * p by POLYNOM3:def 10;

then q = (d * p) + r by B1, POLYNOM3:def 10;

then B2: q - r = (d * p) + (r - r) by RLVECT_1:28

.= (d * p) + (0. (Polynom-Ring F)) by RLVECT_1:15 ;

{p} -Ideal = { (p * c) where c is Element of (Polynom-Ring F) : verum } by IDEAL_1:64;

then p * d in {p} -Ideal ;

then d * p in {p} -Ideal by GROUP_1:def 12;

then Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),r) by B2, RING_1:6;

hence ex r being constant Element of the carrier of (Polynom-Ring F) st Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),r) ; :: thesis: verum

end;B1: q = ((q div p) *' p) + (q mod p) by RING_4:4;

reconsider r = q mod p, d = q div p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

deg r < deg p by divmod;

then deg r < 1 by defl;

then (deg r) + 1 <= 1 by INT_1:7;

then ((deg r) + 1) - 1 <= 1 - 1 by XREAL_1:9;

then reconsider r = r as constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4;

(q div p) *' p = d * p by POLYNOM3:def 10;

then q = (d * p) + r by B1, POLYNOM3:def 10;

then B2: q - r = (d * p) + (r - r) by RLVECT_1:28

.= (d * p) + (0. (Polynom-Ring F)) by RLVECT_1:15 ;

{p} -Ideal = { (p * c) where c is Element of (Polynom-Ring F) : verum } by IDEAL_1:64;

then p * d in {p} -Ideal ;

then d * p in {p} -Ideal by GROUP_1:def 12;

then Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),r) by B2, RING_1:6;

hence ex r being constant Element of the carrier of (Polynom-Ring F) st Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),r) ; :: thesis: verum

E: now :: thesis: for o being object st o in the carrier of ((Polynom-Ring F) / ({p} -Ideal)) holds

o in rng (emb p)

o in rng (emb p)

let o be object ; :: thesis: ( o in the carrier of ((Polynom-Ring F) / ({p} -Ideal)) implies o in rng (emb p) )

assume o in the carrier of ((Polynom-Ring F) / ({p} -Ideal)) ; :: thesis: o in rng (emb p)

then consider q being Element of the carrier of (Polynom-Ring F) such that

E1: o = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) by RING_1:11;

consider r being constant Element of the carrier of (Polynom-Ring F) such that

E2: Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),r) by B;

consider a being Element of F such that

E3: a | F = r by RING_4:20;

E4: (emb p) . a = o by E1, E2, E3, FIELD_1:39;

dom (emb p) = the carrier of F by FUNCT_2:def 1;

hence o in rng (emb p) by E4, FUNCT_1:def 3; :: thesis: verum

end;assume o in the carrier of ((Polynom-Ring F) / ({p} -Ideal)) ; :: thesis: o in rng (emb p)

then consider q being Element of the carrier of (Polynom-Ring F) such that

E1: o = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) by RING_1:11;

consider r being constant Element of the carrier of (Polynom-Ring F) such that

E2: Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),r) by B;

consider a being Element of F such that

E3: a | F = r by RING_4:20;

E4: (emb p) . a = o by E1, E2, E3, FIELD_1:39;

dom (emb p) = the carrier of F by FUNCT_2:def 1;

hence o in rng (emb p) by E4, FUNCT_1:def 3; :: thesis: verum

now :: thesis: for o being object st o in rng (emb p) holds

o in the carrier of ((Polynom-Ring F) / ({p} -Ideal))

then C:
rng (emb p) = the carrier of ((Polynom-Ring F) / ({p} -Ideal))
by E, TARSKI:2;o in the carrier of ((Polynom-Ring F) / ({p} -Ideal))

let o be object ; :: thesis: ( o in rng (emb p) implies o in the carrier of ((Polynom-Ring F) / ({p} -Ideal)) )

assume B: o in rng (emb p) ; :: thesis: o in the carrier of ((Polynom-Ring F) / ({p} -Ideal))

rng (emb p) c= the carrier of ((Polynom-Ring F) / ({p} -Ideal)) by RELAT_1:def 19;

hence o in the carrier of ((Polynom-Ring F) / ({p} -Ideal)) by B; :: thesis: verum

end;assume B: o in rng (emb p) ; :: thesis: o in the carrier of ((Polynom-Ring F) / ({p} -Ideal))

rng (emb p) c= the carrier of ((Polynom-Ring F) / ({p} -Ideal)) by RELAT_1:def 19;

hence o in the carrier of ((Polynom-Ring F) / ({p} -Ideal)) by B; :: thesis: verum

X: ( [#] F = the carrier of F & [#] ((Polynom-Ring F) / ({p} -Ideal)) = the carrier of ((Polynom-Ring F) / ({p} -Ideal)) ) ;

thus the carrier of (embField (emb p)) = carr (emb p) by FIELD_2:def 7

.= ( the carrier of ((Polynom-Ring F) / ({p} -Ideal)) \ (rng (emb p))) \/ the carrier of F by X, FIELD_2:def 2

.= {} \/ the carrier of F by C, XBOOLE_1:37

.= the carrier of F ; :: thesis: verum