let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R holds gcd ((a * c),(b * c),Amp) is_associated_to c * (gcd (a,b,Amp))
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R holds gcd ((a * c),(b * c),Amp) is_associated_to c * (gcd (a,b,Amp))
let A, B, C be Element of R; :: thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))

now :: thesis: ( ( C <> 0. R & gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ) or ( C = 0. R & gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ) )

per cases ( C <> 0. R or C = 0. R ) ;

case A1: C <> 0. R ; :: thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))

set D = gcd (A,B,Amp);

now :: thesis: ( ( gcd (A,B,Amp) <> 0. R & gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ) or ( gcd (A,B,Amp) = 0. R & gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ) )

per cases ( gcd (A,B,Amp) <> 0. R or gcd (A,B,Amp) = 0. R ) ;

case A2: gcd (A,B,Amp) <> 0. R ; :: thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))

set E = gcd ((A * C),(B * C),Amp);
A3: gcd ((A * C),(B * C),Amp) divides B * C by Def12;
gcd (A,B,Amp) divides B by Def12;
then A4: C * (gcd (A,B,Amp)) divides B * C by Th5;
gcd (A,B,Amp) divides A by Def12;
then C * (gcd (A,B,Amp)) divides A * C by Th5;
then C * (gcd (A,B,Amp)) divides gcd ((A * C),(B * C),Amp) by A4, Def12;
then consider F being Element of R such that
A5: gcd ((A * C),(B * C),Amp) = (C * (gcd (A,B,Amp))) * F ;
A6: gcd ((A * C),(B * C),Amp) divides A * C by Def12;
( (gcd (A,B,Amp)) * F divides A & (gcd (A,B,Amp)) * F divides B )

proof

consider G being Element of R such that
A7: ((C * (gcd (A,B,Amp))) * F) * G = A * C by A5, A6;
(C * ((gcd (A,B,Amp)) * F)) * G = C * A by A7, GROUP_1:def 3;
then A8: C * ((gcd (A,B,Amp)) * F) divides C * A ;
consider G being Element of R such that
A9: ((C * (gcd (A,B,Amp))) * F) * G = B * C by A5, A3;
(C * ((gcd (A,B,Amp)) * F)) * G = C * B by A9, GROUP_1:def 3;
then C * ((gcd (A,B,Amp)) * F) divides C * B ;
hence ( (gcd (A,B,Amp)) * F divides A & (gcd (A,B,Amp)) * F divides B ) by A1, A8, Th15; :: thesis: verum

end;

then A10: (gcd (A,B,Amp)) * F divides gcd (A,B,Amp) by Def12;
gcd (A,B,Amp) = (gcd (A,B,Amp)) * (1. R) ;
then F divides 1. R by A2, A10, Th15;
then ex y being Element of R st 1. R = F * y ;
then F is unital ;
hence gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) by A5, Th18; :: thesis: verum

end;

case A11: gcd (A,B,Amp) = 0. R ; :: thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))

then A12: C * (gcd (A,B,Amp)) = 0. R ;
( A = 0. R & B = 0. R ) by A11, Th33;
then gcd ((A * C),(B * C),Amp) = gcd ((0. R),((0. R) * C),Amp)
.= gcd ((0. R),(0. R),Amp)
.= C * (gcd (A,B,Amp)) by A12, Th31 ;
hence gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; :: thesis: verum

end;

end;

end;

hence gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; :: thesis: verum

end;

case A13: C = 0. R ; :: thesis: gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp))

then ( A * C = 0. R & B * C = 0. R ) ;
then gcd ((A * C),(B * C),Amp) = 0. R by Th31
.= C * (gcd (A,B,Amp)) by A13 ;
hence gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; :: thesis: verum

end;

end;

end;

hence gcd ((A * C),(B * C),Amp) is_associated_to C * (gcd (A,B,Amp)) ; :: thesis: verum