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;
( gcd A,B,Amp divides A & gcd A,B,Amp divides B ) by Def12;
then ( C * (gcd A,B,Amp) divides A * C & C * (gcd A,B,Amp) divides B * C ) by Th5;
then C * (gcd A,B,Amp) divides gcd (A * C),(B * C),Amp by Def12;
then consider F being Element of R such that
A3: gcd (A * C),(B * C),Amp = (C * (gcd A,B,Amp)) * F by Def1;
A4: gcd (A * C),(B * C),Amp divides A * C by Def12;
A5: gcd (A * C),(B * C),Amp divides B * 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
A6: ((C * (gcd A,B,Amp)) * F) * G = A * C by A3, A4, Def1;
(C * ((gcd A,B,Amp) * F)) * G = C * A by A6, GROUP_1:def 4;
then A7: C * ((gcd A,B,Amp) * F) divides C * A by Def1;
consider G being Element of R such that
A8: ((C * (gcd A,B,Amp)) * F) * G = B * C by A3, A5, Def1;
(C * ((gcd A,B,Amp) * F)) * G = C * B by A8, 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, A7, Th15; :: thesis: verum

end;

then A9: (gcd A,B,Amp) * F divides gcd A,B,Amp by Def12;
F divides 1. R

proof

gcd A,B,Amp = (gcd A,B,Amp) * (1. R) by VECTSP_1:def 13;
hence F divides 1. R by A2, A9, Th15; :: thesis: verum

end;

then F is unital by Def2;
hence gcd (A * C),(B * C),Amp is_associated_to C * (gcd A,B,Amp) by A3, Th18; :: thesis: verum

end;

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

then A11: ( A = 0. R & B = 0. R ) by Th34;
A12: C * (gcd A,B,Amp) = 0. R by A10, VECTSP_1:39;
gcd (A * C),(B * C),Amp = gcd (0. R),((0. R) * C),Amp by A11, 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 A14: A * C = 0. R by VECTSP_1:39;
B * C = 0. R by A13, VECTSP_1:39;
then gcd (A * C),(B * C),Amp = 0. R by A14, 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