theorem Th25: :: GCD_1:25

for R being commutative domRing-like Ring
for Amp being AmpleSet of R holds
( NF ((0. R),Amp) = 0. R & NF ((1. R),Amp) = 1. R )