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 gcd A,B,Amp = 1. R ; :: thesis: gcd A,(B * C),Amp = gcd A,C,Amp
then A1: C * (gcd A,B,Amp) = C by VECTSP_1:def 13;
gcd (A * C),(B * C),Amp is_associated_to C * (gcd A,B,Amp) by Th37;
then gcd A,C,Amp is_associated_to gcd A,(gcd (A * C),(B * C),Amp),Amp by A1, Th35;
then A2: gcd A,C,Amp is_associated_to gcd (gcd A,(A * C),Amp),(B * C),Amp by Th36;
A3: A * (gcd (1. R),C,Amp) = A * (1. R) by Th33
.= A by VECTSP_1:def 13 ;
gcd (A * (1. R)),(A * C),Amp is_associated_to A * (gcd (1. R),C,Amp) by Th37;
then gcd A,(A * C),Amp is_associated_to A by A3, VECTSP_1:def 13;
then A4: gcd (gcd A,(A * C),Amp),(B * C),Amp is_associated_to gcd A,(B * C),Amp by Th35;
( gcd A,(B * C),Amp is Element of Amp & gcd A,C,Amp is Element of Amp ) by Def12;
hence gcd A,(B * C),Amp = gcd A,C,Amp by A2, A4, Th4, Th22; :: thesis: verum