for R being gcdDomain
for Amp being AmpleSet of R
for a being Element of R holds
( gcd (a,(0. R),Amp) = NF (a,Amp) & gcd ((0. R),a,Amp) = NF (a,Amp) )