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;
( gcd (gcd A,B,Amp),C,Amp divides gcd A,B,Amp & gcd (gcd A,B,Amp),C,Amp divides C ) by Def12;
then ( gcd (gcd A,B,Amp),C,Amp divides A & gcd (gcd A,B,Amp),C,Amp divides B & gcd (gcd A,B,Amp),C,Amp divides C ) by Th29;
then ( gcd (gcd A,B,Amp),C,Amp divides A & gcd (gcd A,B,Amp),C,Amp divides gcd B,C,Amp ) by Def12;
then A1: gcd (gcd A,B,Amp),C,Amp divides gcd A,(gcd B,C,Amp),Amp by Def12;
( gcd A,(gcd B,C,Amp),Amp divides gcd B,C,Amp & gcd A,(gcd B,C,Amp),Amp divides A ) by Def12;
then ( gcd A,(gcd B,C,Amp),Amp divides B & gcd A,(gcd B,C,Amp),Amp divides C & gcd A,(gcd B,C,Amp),Amp divides A ) by Th29;
then ( gcd A,(gcd B,C,Amp),Amp divides C & gcd A,(gcd B,C,Amp),Amp divides gcd A,B,Amp ) by Def12;
then gcd A,(gcd B,C,Amp),Amp divides gcd (gcd A,B,Amp),C,Amp by Def12;
then A2: gcd (gcd A,B,Amp),C,Amp is_associated_to gcd A,(gcd B,C,Amp),Amp by A1, Def3;
A3: gcd (gcd A,B,Amp),C,Amp is Element of Amp by Def12;
gcd A,(gcd B,C,Amp),Amp is Element of Amp by Def12;
hence gcd (gcd A,B,Amp),C,Amp = gcd A,(gcd B,C,Amp),Amp by A2, A3, Th22; :: thesis: verum