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;

A: now :: thesis: for o being object st o in the carrier of (Polynom-Ring p) holds
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;

X: now :: thesis: for o being object st o in rng (canHomP p) holds
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;

then B: rng (canHomP p) = the carrier of (Polynom-Ring p) by A, TARSKI:2;
( 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