let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R holds gcd (gcd a,b,Amp),c,Amp = gcd a,(gcd b,c,Amp),Amp
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R holds gcd (gcd a,b,Amp),c,Amp = gcd a,(gcd b,c,Amp),Amp
let A, B, C be Element of R; :: thesis: gcd (gcd A,B,Amp),C,Amp = gcd A,(gcd B,C,Amp),Amp
set D = gcd (gcd A,B,Amp),C,Amp;
set E = gcd A,(gcd B,C,Amp),Amp;
A1: gcd (gcd A,B,Amp),C,Amp divides C by Def12;
A2: gcd A,(gcd B,C,Amp),Amp divides A by Def12;
A3: gcd A,(gcd B,C,Amp),Amp divides gcd B,C,Amp by Def12;
then A4: gcd A,(gcd B,C,Amp),Amp divides C by Th29;
gcd A,(gcd B,C,Amp),Amp divides B by A3, Th29;
then gcd A,(gcd B,C,Amp),Amp divides gcd A,B,Amp by A2, Def12;
then A5: gcd A,(gcd B,C,Amp),Amp divides gcd (gcd A,B,Amp),C,Amp by A4, Def12;
A6: ( gcd (gcd A,B,Amp),C,Amp is Element of Amp & gcd A,(gcd B,C,Amp),Amp is Element of Amp ) by Def12;
A7: gcd (gcd A,B,Amp),C,Amp divides gcd A,B,Amp by Def12;
then A8: gcd (gcd A,B,Amp),C,Amp divides A by Th29;
gcd (gcd A,B,Amp),C,Amp divides B by A7, Th29;
then gcd (gcd A,B,Amp),C,Amp divides gcd B,C,Amp by A1, Def12;
then gcd (gcd A,B,Amp),C,Amp divides gcd A,(gcd B,C,Amp),Amp by A8, Def12;
then gcd (gcd A,B,Amp),C,Amp is_associated_to gcd A,(gcd B,C,Amp),Amp by A5, Def3;
hence gcd (gcd A,B,Amp),C,Amp = gcd A,(gcd B,C,Amp),Amp by A6, Th22; :: thesis: verum