A1: ( KroneckerIso p is linear & KroneckerIso p is one-to-one ) ;
hence KroneckerField (F,p) is Polynom-Ring p -homomorphic by RING_2:def 4; :: thesis: ( KroneckerField (F,p) is Polynom-Ring p -monomorphic & KroneckerField (F,p) is Polynom-Ring p -isomorphic )
thus KroneckerField (F,p) is Polynom-Ring p -monomorphic by A1, RING_3:def 3; :: thesis: KroneckerField (F,p) is Polynom-Ring p -isomorphic
thus KroneckerField (F,p) is Polynom-Ring p -isomorphic by A1, RING_3:def 4; :: thesis: verum