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

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

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 by Def1;
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, Def1;
(C * ((gcd A,B,Amp) * F)) * G = C * A by A7, GROUP_1:def 4;
then A8: C * ((gcd A,B,Amp) * F) divides C * A by Def1;
consider G being Element of R such that
A9: ((C * (gcd A,B,Amp)) * F) * G = B * C by A5, A3, Def1;
(C * ((gcd A,B,Amp) * F)) * G = C * B by A9, GROUP_1:def 4;
then C * ((gcd A,B,Amp) * F) divides C * B by Def1;
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) by VECTSP_1:def 13;
then F divides 1. R by A2, A10, Th15;
then F is unital by Def2;
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 by VECTSP_1:39;
( A = 0. R & B = 0. R ) by A11, Th34;
then gcd (A * C),(B * C),Amp = gcd (0. R),((0. R) * C),Amp by VECTSP_1:39
.= gcd (0. R),(0. R),Amp by VECTSP_1:39
.= C * (gcd A,B,Amp) by A12, Th32 ;
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 ) by VECTSP_1:39;
then gcd (A * C),(B * C),Amp = 0. R by Th32
.= C * (gcd A,B,Amp) by A13, VECTSP_1:39 ;
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