:: deftheorem Def4 defines frac1 RINGFRAC:def 9 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for b₃ being Function of R,(Frac S) holds
( b₃ = frac1 S iff for o being object st o in the carrier of R holds
b₃ . o = [o,(1. R)] );