let R be EuclidianRing; :: thesis: 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)
let a, b be Element of R; :: thesis: for g being a_gcd of a,b ex r, s being Element of R st g = (a * r) + (b * s)
let g be a_gcd of a,b; :: thesis: ex r, s being Element of R st g = (a * r) + (b * s)

per cases ( a is zero or not a is zero ) ;

suppose a is zero ; :: thesis: ex r, s being Element of R st g = (a * r) + (b * s)

then g is_associated_to b by lemgcd0;
then consider c being Element of R such that
A: ( c is unital & b * c = g ) by GCD_1:18;
take 0. R ; :: thesis: ex s being Element of R st g = (a * (0. R)) + (b * s)
take c ; :: thesis: g = (a * (0. R)) + (b * c)
thus g = (a * (0. R)) + (b * c) by A; :: thesis: verum

end;

suppose S: not a is zero ; :: thesis: ex r, s being Element of R st g = (a * r) + (b * s)

set f = the DegreeFunction of R;
defpred S₁[ Nat] means ex d being Element of R st
( $1 = the DegreeFunction of R . d & d in {a,b} -Ideal & {d} -Ideal <> {(0. R)} );
A: ex k being Nat st S₁[k]

proof

{a,b} -Ideal is principal by IDEAL_1:def 28;
then consider d being Element of R such that
A1: {d} -Ideal = {a,b} -Ideal ;

A3: now :: thesis: not {d} -Ideal = {(0. R)}

assume A4: {d} -Ideal = {(0. R)} ; :: thesis: contradiction
( a <> 0. R & a in {d} -Ideal ) by S, A1, IDEAL_1:68;
hence contradiction by A4, TARSKI:def 1; :: thesis: verum

end;

take the DegreeFunction of R . d ; :: thesis: S₁[ the DegreeFunction of R . d]
thus S₁[ the DegreeFunction of R . d] by A1, A3, IDEAL_1:66; :: thesis: verum

end;

consider k being Nat such that
B: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A);
consider d being Element of R such that
H1: ( the DegreeFunction of R . d = k & d in {a,b} -Ideal & {d} -Ideal <> {(0. R)} ) by B;
H2: ( {d} -Ideal = { (d * r) where r is Element of R : verum } & {a,b} -Ideal = { ((a * r) + (b * s)) where r, s is Element of R : verum } ) by IDEAL_1:64, IDEAL_1:65;
then consider s, t being Element of R such that
H3: d = (a * s) + (b * t) by H1;
d is a_gcd of a,b

proof

B0: d <> 0. R by H1, IDEAL_1:48;
then consider q, r being Element of R such that
B1: ( a = (q * d) + r & ( r = 0. R or the DegreeFunction of R . r < the DegreeFunction of R . d ) ) by INT_3:def 9;

now :: thesis: not r <> 0. R

assume B2: r <> 0. R ; :: thesis: contradiction

B4: now :: thesis: not {r} -Ideal = {(0. R)}

assume B5: {r} -Ideal = {(0. R)} ; :: thesis: contradiction
r in {r} -Ideal by IDEAL_1:66;
hence contradiction by B2, B5, TARSKI:def 1; :: thesis: verum

end;

r = a - (q * ((a * s) + (b * t))) by H3, B1, VECTSP_2:2
.= a + ((- q) * ((a * s) + (b * t))) by VECTSP_1:9
.= a + (((- q) * (a * s)) + ((- q) * (b * t))) by VECTSP_1:def 2
.= (a + ((- q) * (a * s))) + ((- q) * (b * t)) by RLVECT_1:def 3
.= ((a * (1. R)) + (a * ((- q) * s))) + ((- q) * (b * t)) by GROUP_1:def 3
.= (a * ((1. R) + ((- q) * s))) + ((- q) * (b * t)) by VECTSP_1:def 2
.= (a * ((1. R) + ((- q) * s))) + (b * ((- q) * t)) by GROUP_1:def 3 ;
then r in {a,b} -Ideal by H2;
hence contradiction by B1, B2, B4, B, H1; :: thesis: verum

end;

then B2: d divides a by B1, GCD_1:def 1;
consider q, r being Element of R such that
B1: ( b = (q * d) + r & ( r = 0. R or the DegreeFunction of R . r < the DegreeFunction of R . d ) ) by B0, INT_3:def 9;

now :: thesis: not r <> 0. R

assume B2: r <> 0. R ; :: thesis: contradiction

B4: now :: thesis: not {r} -Ideal = {(0. R)}

assume B5: {r} -Ideal = {(0. R)} ; :: thesis: contradiction
r in {r} -Ideal by IDEAL_1:66;
hence contradiction by B2, B5, TARSKI:def 1; :: thesis: verum

end;

r = b - (q * ((a * s) + (b * t))) by H3, B1, VECTSP_2:2
.= b + ((- q) * ((a * s) + (b * t))) by VECTSP_1:9
.= b + (((- q) * (b * t)) + ((- q) * (a * s))) by VECTSP_1:def 2
.= (b + ((- q) * (b * t))) + ((- q) * (a * s)) by RLVECT_1:def 3
.= ((b * (1. R)) + (b * ((- q) * t))) + ((- q) * (a * s)) by GROUP_1:def 3
.= (b * ((1. R) + ((- q) * t))) + ((- q) * (a * s)) by VECTSP_1:def 2
.= (b * ((1. R) + ((- q) * t))) + (a * ((- q) * s)) by GROUP_1:def 3 ;
then r in {a,b} -Ideal by H2;
hence contradiction by B1, B2, B4, B, H1; :: thesis: verum

end;

then B3: d divides b by B1, GCD_1:def 1;

now :: thesis: for x being Element of R st x divides a & x divides b holds
x divides d

let x be Element of R; :: thesis: ( x divides a & x divides b implies x divides d )
assume B4: ( x divides a & x divides b ) ; :: thesis: x divides d
then consider c being Element of R such that
B5: x * c = a * s by GCD_1:def 1, GCD_1:7;
consider e being Element of R such that
B6: x * e = b * t by B4, GCD_1:def 1, GCD_1:7;
x * (c + e) = (x * c) + (x * e) by VECTSP_1:def 2;
hence x divides d by H3, B6, B5, GCD_1:def 1; :: thesis: verum

end;

hence d is a_gcd of a,b by B2, B3, RING_4:def 10; :: thesis: verum

end;

then H3: {g} -Ideal = {d} -Ideal by RING_2:21, RING_4:49;
H5: {d} -Ideal c= {a,b} -Ideal by H1, IDEAL_1:67;
g in {a,b} -Ideal by H3, H5, IDEAL_1:66;
hence ex r, s being Element of R st g = (a * r) + (b * s) by H2; :: thesis: verum

end;

end;