:: deftheorem defines *' ARYTM_3:def 12 :
for x, y being Element of RAT+ holds x *' y = ((numerator x) *^ (numerator y)) / ((denominator x) *^ (denominator y));