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