theorem :: RINGFRAC:41

for A, B being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A
for f being Function of A,B st f is RingHomomorphism & f .: S c= Unit_Set B holds
Univ_Map (S,f) is RingHomomorphism by Th57, Th58, Th59;