let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds (Polynom-Ring F) / ({p} -Ideal), Polynom-Ring p are_isomorphic
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: (Polynom-Ring F) / ({p} -Ideal), Polynom-Ring p are_isomorphic
set R = Polynom-Ring F;
set S = Polynom-Ring p;
(Polynom-Ring F) / (ker (poly_mod p)), Polynom-Ring p are_isomorphic by RING_2:16;
hence (Polynom-Ring F) / ({p} -Ideal), Polynom-Ring p are_isomorphic by kerp; :: thesis: verum