let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R st b is_associated_to c holds
( gcd a,b,Amp is_associated_to gcd a,c,Amp & gcd b,a,Amp is_associated_to gcd c,a,Amp )
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R st b is_associated_to c holds
( gcd a,b,Amp is_associated_to gcd a,c,Amp & gcd b,a,Amp is_associated_to gcd c,a,Amp )
let A, B, C be Element of R; :: thesis: ( B is_associated_to C implies ( gcd A,B,Amp is_associated_to gcd A,C,Amp & gcd B,A,Amp is_associated_to gcd C,A,Amp ) )
assume A1: B is_associated_to C ; :: thesis: ( gcd A,B,Amp is_associated_to gcd A,C,Amp & gcd B,A,Amp is_associated_to gcd C,A,Amp )
then A2: B divides C by Def3;
gcd A,B,Amp divides B by Def12;
then A3: gcd A,B,Amp divides C by A2, Th2;
gcd A,B,Amp divides A by Def12;
then A4: gcd A,B,Amp divides gcd A,C,Amp by A3, Def12;
A5: gcd A,B,Amp = gcd B,A,Amp by Th30;
A6: C divides B by A1, Def3;
gcd A,C,Amp divides C by Def12;
then A7: gcd A,C,Amp divides B by A6, Th2;
gcd A,C,Amp divides A by Def12;
then gcd A,C,Amp divides gcd A,B,Amp by A7, Def12;
then gcd A,B,Amp is_associated_to gcd A,C,Amp by A4, Def3;
hence ( gcd A,B,Amp is_associated_to gcd A,C,Amp & gcd B,A,Amp is_associated_to gcd C,A,Amp ) by A5, Th30; :: thesis: verum