set K = KroneckerField (F,p);
E9: emb_iso (canHomP p) is onto by lemdis, FIELD_2:15;
rng (KroneckerIso p) = the carrier of (KroneckerField (F,p)) by FUNCT_2:def 3;
then KrRoot p in rng (KroneckerIso p) ;
then E3: KrRoot p in dom ((KroneckerIso p) ") by FUNCT_1:32;
then E6: ((KroneckerIso p) ") . (KrRoot p) in rng ((KroneckerIso p) ") by FUNCT_1:def 3;
E10: ((KroneckerIso p) ") . (KrRoot p) in dom (KroneckerIso p) by E6, FUNCT_1:33;
dom ((emb_iso (canHomP p)) ") = the carrier of (Polynom-Ring p) by E9, FUNCT_1:33
.= dom (KroneckerIso p) by FUNCT_2:def 1 ;
then ((emb_iso (canHomP p)) ") . (((KroneckerIso p) ") . (KrRoot p)) in rng ((emb_iso (canHomP p)) ") by E10, FUNCT_1:3;
then ((emb_iso (canHomP p)) ") . (((KroneckerIso p) ") . (KrRoot p)) in dom (emb_iso (canHomP p)) by FUNCT_1:33;
hence (((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p) is Element of (embField (canHomP p)) by E3, FUNCT_1:13; :: thesis: verum