:: deftheorem Def7 defines canHom RINGFRAC:def 19 :
for A being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A
for b₃ being Function of A,(S ~ A) holds
( b₃ = canHom S iff for o being object st o in the carrier of A holds
b₃ . o = Class ((EqRel S),((frac1 S) . o)) );