theorem lemgcdii: :: FIELD_14:43

for R being EuclidianRing
for a, b being Element of R
for g being a_gcd of a,b ex r, s being Element of R st g = (a * r) + (b * s)