:: deftheorem Def05 defines RAT_ratio MUSIC_S1:def 9 :
for b₁ being Function of [:RATPLUS,RATPLUS:],RATPLUS holds
( b₁ = RAT_ratio iff for x being Element of [:RATPLUS,RATPLUS:] ex y, z being Element of RATPLUS st
( x = [y,z] & b₁ . x = RAT_ratio (y,z) ) );