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

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