for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st Amp is multiplicative & r1,r2 are_normalized_wrt Amp & s1,s2 are_normalized_wrt Amp holds
add1 (r1,r2,s1,s2,Amp), add2 (r1,r2,s1,s2,Amp) are_normalized_wrt Amp