:: deftheorem defines Fracadd RINGFRAC:def 10 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for u, v being Element of Frac S holds Fracadd (u,v) = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))];