theorem :: RINGFRAC:33

for A being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A st not 0. A in S & A is domRing holds
( ker (canHom S) = {(0. A)} & canHom S is one-to-one )