set R = (Polynom-Ring F) / ({p} -Ideal);
set S = Polynom-Ring p;
ex f being Function of ((Polynom-Ring F) / ({p} -Ideal)),(Polynom-Ring p) st f is RingIsomorphism by ISO, QUOFIELD:def 23;
then Polynom-Ring p is (Polynom-Ring F) / ({p} -Ideal) -isomorphic by RING_3:def 4;
hence Polynom-Ring p is almost_left_invertible ; :: thesis: verum