:: deftheorem Def19 defines mult2 GCD_1:def 19 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF (r2,Amp) & s2 = NF (s2,Amp) holds
( ( ( r1 = 0. R or s1 = 0. R ) implies mult2 (r1,r2,s1,s2,Amp) = 1. R ) & ( r2 = 1. R & s2 = 1. R implies mult2 (r1,r2,s1,s2,Amp) = 1. R ) & ( s2 <> 0. R & r2 = 1. R implies mult2 (r1,r2,s1,s2,Amp) = s2 / (gcd (r1,s2,Amp)) ) & ( r2 <> 0. R & s2 = 1. R implies mult2 (r1,r2,s1,s2,Amp) = r2 / (gcd (s1,r2,Amp)) ) & ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or mult2 (r1,r2,s1,s2,Amp) = (r2 / (gcd (s1,r2,Amp))) * (s2 / (gcd (r1,s2,Amp))) ) );