let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b, c being Element of R holds gcd (a + (b * c)),c,Amp = gcd a,c,Amp
let Amp be AmpleSet of R; :: thesis: for a, b, c being Element of R holds gcd (a + (b * c)),c,Amp = gcd a,c,Amp
let A, B, C be Element of R; :: thesis: gcd (A + (B * C)),C,Amp = gcd A,C,Amp
set D = gcd A,C,Amp;
A1: ( gcd A,C,Amp divides A & gcd A,C,Amp divides C ) by Def12;
A2: gcd A,C,Amp is Element of Amp by Def12;
consider E being Element of R such that
A3: (gcd A,C,Amp) * E = A by A1, Def1;
consider F being Element of R such that
A4: (gcd A,C,Amp) * F = C by A1, Def1;
A5: gcd A,C,Amp divides A + (B * C)

proof

(gcd A,C,Amp) * (E + (F * B)) = ((gcd A,C,Amp) * E) + ((gcd A,C,Amp) * (F * B)) by VECTSP_1:def 11
.= A + (B * C) by A3, A4, GROUP_1:def 4 ;
hence gcd A,C,Amp divides A + (B * C) by Def1; :: thesis: verum

end;

for z being Element of R st z divides A + (B * C) & z divides C holds
z divides gcd A,C,Amp

proof

let Z be Element of R; :: thesis: ( Z divides A + (B * C) & Z divides C implies Z divides gcd A,C,Amp )
assume A6: ( Z divides A + (B * C) & Z divides C ) ; :: thesis: Z divides gcd A,C,Amp
then consider X being Element of R such that
A7: Z * X = C by Def1;
consider Y being Element of R such that
A8: Z * Y = A + (B * C) by A6, Def1;
Z * (Y + (- (B * X))) = (Z * Y) + (Z * (- (B * X))) by VECTSP_1:def 11
.= (Z * Y) + (- (Z * (X * B))) by VECTSP_1:40
.= (A + (B * C)) + (- (C * B)) by A7, A8, GROUP_1:def 4
.= A + ((B * C) + (- (C * B))) by RLVECT_1:def 6
.= A + (0. R) by RLVECT_1:def 11
.= A by RLVECT_1:10 ;
then Z divides A by Def1;
hence Z divides gcd A,C,Amp by A6, Def12; :: thesis: verum

end;

hence gcd (A + (B * C)),C,Amp = gcd A,C,Amp by A1, A2, A5, Def12; :: thesis: verum