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

( Polynom-Ring p,F are_isomorphic & the carrier of (embField (canHomP p)) = the carrier of F )

let p be linear Element of the carrier of (Polynom-Ring F); :: thesis: ( Polynom-Ring p,F are_isomorphic & the carrier of (embField (canHomP p)) = the carrier of F )

set FP = Polynom-Ring p;

set f = canHomP p;

H: the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;

( canHomP p is monomorphism & canHomP p is onto ) by X, A, TARSKI:2;

then F, Polynom-Ring p are_isomorphic ;

hence Polynom-Ring p,F are_isomorphic ; :: thesis: the carrier of (embField (canHomP p)) = the carrier of F

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

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

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

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

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

( Polynom-Ring p,F are_isomorphic & the carrier of (embField (canHomP p)) = the carrier of F )

let p be linear Element of the carrier of (Polynom-Ring F); :: thesis: ( Polynom-Ring p,F are_isomorphic & the carrier of (embField (canHomP p)) = the carrier of F )

set FP = Polynom-Ring p;

set f = canHomP p;

H: the carrier of (Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;

A: now :: thesis: for o being object st o in the carrier of (Polynom-Ring p) holds

o in rng (canHomP p)

o in rng (canHomP p)

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring p) implies o in rng (canHomP p) )

assume o in the carrier of (Polynom-Ring p) ; :: thesis: o in rng (canHomP p)

then consider q being Polynomial of F such that

B: ( q = o & deg q < deg p ) by H;

reconsider q = q as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

deg q < 1 by B, defl;

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

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

then consider a being Element of F such that

C: q = a | F by RING_4:20, RING_4:def 4;

D: (canHomP p) . a = o by B, C, defch;

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

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

end;assume o in the carrier of (Polynom-Ring p) ; :: thesis: o in rng (canHomP p)

then consider q being Polynomial of F such that

B: ( q = o & deg q < deg p ) by H;

reconsider q = q as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

deg q < 1 by B, defl;

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

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

then consider a being Element of F such that

C: q = a | F by RING_4:20, RING_4:def 4;

D: (canHomP p) . a = o by B, C, defch;

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

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

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

o in the carrier of (Polynom-Ring p)

then B:
rng (canHomP p) = the carrier of (Polynom-Ring p)
by A, TARSKI:2;o in the carrier of (Polynom-Ring p)

let o be object ; :: thesis: ( o in rng (canHomP p) implies o in the carrier of (Polynom-Ring p) )

assume B: o in rng (canHomP p) ; :: thesis: o in the carrier of (Polynom-Ring p)

rng (canHomP p) c= the carrier of (Polynom-Ring p) by RELAT_1:def 19;

hence o in the carrier of (Polynom-Ring p) by B; :: thesis: verum

end;assume B: o in rng (canHomP p) ; :: thesis: o in the carrier of (Polynom-Ring p)

rng (canHomP p) c= the carrier of (Polynom-Ring p) by RELAT_1:def 19;

hence o in the carrier of (Polynom-Ring p) by B; :: thesis: verum

( canHomP p is monomorphism & canHomP p is onto ) by X, A, TARSKI:2;

then F, Polynom-Ring p are_isomorphic ;

hence Polynom-Ring p,F are_isomorphic ; :: thesis: the carrier of (embField (canHomP p)) = the carrier of F

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

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

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

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

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