set f = emb (F,I,g);
emb (F,I,g) is monomorphism ;
hence KroneckerField (F,g,I) is F -monomorphic by RING_3:def 3; :: thesis: KroneckerField (F,g,I) is F -homomorphic
hence KroneckerField (F,g,I) is F -homomorphic ; :: thesis: verum