let K be Field; :: thesis: for f, g being Element of (Polynom-Ring K) st f <> 0. (Polynom-Ring K) & {f} -Ideal is prime & not g in {f} -Ideal holds
{f,g} -Ideal = the carrier of (Polynom-Ring K)
let f, g be Element of (Polynom-Ring K); :: thesis: ( f <> 0. (Polynom-Ring K) & {f} -Ideal is prime & not g in {f} -Ideal implies {f,g} -Ideal = the carrier of (Polynom-Ring K) )
assume that
A1: f <> 0. (Polynom-Ring K) and
A2: {f} -Ideal is prime and
A4: not g in {f} -Ideal ; :: thesis: {f,g} -Ideal = the carrier of (Polynom-Ring K)
assume A5: {f,g} -Ideal <> the carrier of (Polynom-Ring K) ; :: thesis: contradiction
Polynom-Ring K is PID ;
then consider h being Element of (Polynom-Ring K) such that
A7: {f,g} -Ideal = {h} -Ideal by IDEAL_1:def 27;
A8: ( {f} -Ideal c= {h} -Ideal & {g} -Ideal c= {h} -Ideal ) by A7, IDEAL_1:69;
consider s being Element of (Polynom-Ring K) such that
A9: f = h * s by RING_2:19, A8, GCD_1:def 1;
consider t being Element of (Polynom-Ring K) such that
A11: g = h * t by RING_2:19, A8, GCD_1:def 1;
f is non zero Element of (Polynom-Ring K) by A1, STRUCT_0:def 12;
then A13: f is prime by A2, RING_2:24;

per cases ( f divides s or f divides h ) by A9, A13;

suppose f divides s ; :: thesis: contradiction

then consider u being Element of (Polynom-Ring K) such that
A16: s = f * u by GCD_1:def 1;
A17: f = f * (u * h) by GROUP_1:def 3, A9, A16;
reconsider v = u * h as Element of (Polynom-Ring K) ;
(f * (1. (Polynom-Ring K))) - (f * v) = 0. (Polynom-Ring K) by RLVECT_1:5, A17;
then f * ((1. (Polynom-Ring K)) - v) = 0. (Polynom-Ring K) by VECTSP_1:11;
then (1. (Polynom-Ring K)) + (- v) = 0. (Polynom-Ring K) by A1, VECTSP_2:def 1;
then h divides 1. (Polynom-Ring K) by VECTSP_1:19, GCD_1:def 1;
then A27: h is Unit of (Polynom-Ring K) by GCD_1:def 20;
[#] (Polynom-Ring K) = the carrier of (Polynom-Ring K) ;
hence contradiction by A5, A7, A27, RING_2:20; :: thesis: verum

end;

suppose f divides h ; :: thesis: contradiction

then consider v being Element of (Polynom-Ring K) such that
A31: h = f * v by GCD_1:def 1;
g = f * (v * t) by A11, A31, GROUP_1:def 3;
hence contradiction by A4, GCD_1:def 1, RING_2:18; :: thesis: verum

end;

end;