let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R st gcd a,b,Amp = 1. R holds
gcd a,(b * c),Amp = gcd a,c,Amp
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R st gcd a,b,Amp = 1. R holds
gcd a,(b * c),Amp = gcd a,c,Amp
let A, B, C be Element of R; :: thesis: ( gcd A,B,Amp = 1. R implies gcd A,(B * C),Amp = gcd A,C,Amp )
assume A1: gcd A,B,Amp = 1. R ; :: thesis: gcd A,(B * C),Amp = gcd A,C,Amp
A2: gcd (A * C),(B * C),Amp is_associated_to C * (gcd A,B,Amp) by Th37;
C * (gcd A,B,Amp) = C by A1, VECTSP_1:def 13;
then gcd A,C,Amp is_associated_to gcd A,(gcd (A * C),(B * C),Amp),Amp by A2, Th35;
then A3: gcd A,C,Amp is_associated_to gcd (gcd A,(A * C),Amp),(B * C),Amp by Th36;
gcd A,(A * C),Amp is_associated_to A

proof

A4: gcd (A * (1. R)),(A * C),Amp is_associated_to A * (gcd (1. R),C,Amp) by Th37;
A * (gcd (1. R),C,Amp) = A * (1. R) by Th33
.= A by VECTSP_1:def 13 ;
hence gcd A,(A * C),Amp is_associated_to A by A4, VECTSP_1:def 13; :: thesis: verum

end;

then gcd (gcd A,(A * C),Amp),(B * C),Amp is_associated_to gcd A,(B * C),Amp by Th35;
then A5: gcd A,(B * C),Amp is_associated_to gcd A,C,Amp by A3, Th4;
A6: gcd A,(B * C),Amp is Element of Amp by Def12;
gcd A,C,Amp is Element of Amp by Def12;
hence gcd A,(B * C),Amp = gcd A,C,Amp by A5, A6, Th22; :: thesis: verum