for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st gcd (r1,r2,Amp) = 1. R & gcd (s1,s2,Amp) = 1. R & r2 <> 0. R & s2 <> 0. R holds
gcd (((r1 / (gcd (r1,s2,Amp))) * (s1 / (gcd (s1,r2,Amp)))),((r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp)))),Amp) = 1. R