let F be Field; :: thesis: for p, q being Element of (Polynom-Ring F) ex a, b being Element of (Polynom-Ring F) st p gcd q = (a * p) + (b * q)
let p, q be Element of (Polynom-Ring F); :: thesis: ex a, b being Element of (Polynom-Ring F) st p gcd q = (a * p) + (b * q)
set g = p gcd q;
{(p gcd q)} -Ideal = {p,q} -Ideal by lemgcdi;
then A: p gcd q in {p,q} -Ideal by IDEAL_1:66;
{p,q} -Ideal = { ((p * r) + (q * s)) where r, s is Element of (Polynom-Ring F) : verum } by IDEAL_1:65;
then consider r, s being Element of (Polynom-Ring F) such that
B: p gcd q = (p * r) + (q * s) by A;
take r ; :: thesis: ex b being Element of (Polynom-Ring F) st p gcd q = (r * p) + (b * q)
take s ; :: thesis: p gcd q = (r * p) + (s * q)
thus p gcd q = (r * p) + (s * q) by B; :: thesis: verum