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} -Ideal ,{g} -Ideal are_co-prime
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} -Ideal ,{g} -Ideal are_co-prime )
{f,g} -Ideal = ({f} -Ideal) + ({g} -Ideal) by IDEAL_1:76;
hence ( f <> 0. (Polynom-Ring K) & {f} -Ideal is prime & not g in {f} -Ideal implies {f} -Ideal ,{g} -Ideal are_co-prime ) by Th80; :: thesis: verum