:: deftheorem Def8 defines Univ_Map RINGFRAC:def 23 :
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
for b₅ being Function of (S ~ A),B holds
( b₅ = Univ_Map (S,f) iff for x being object st x in the carrier of (S ~ A) holds
ex a, s being Element of A st
( s in S & x = Class ((EqRel S),[a,s]) & b₅ . x = (f . a) * ((f . s) ["]) ) );