reconsider g = (KroneckerIso p) " as Isomorphism of (KroneckerField (F,p)),(Polynom-Ring p) by RING_3:73;
g is Homomorphism of (KroneckerField (F,p)),(Polynom-Ring p) ;
hence Polynom-Ring p is KroneckerField (F,p) -homomorphic by RING_2:def 4; :: thesis: ( Polynom-Ring p is KroneckerField (F,p) -monomorphic & Polynom-Ring p is KroneckerField (F,p) -isomorphic )
g is monomorphism ;
hence Polynom-Ring p is KroneckerField (F,p) -monomorphic by RING_3:def 3; :: thesis: Polynom-Ring p is KroneckerField (F,p) -isomorphic
g is Isomorphism of (KroneckerField (F,p)),(Polynom-Ring p) ;
hence Polynom-Ring p is KroneckerField (F,p) -isomorphic by RING_3:def 4; :: thesis: verum