theorem :: GCD_1:45

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