:: deftheorem Def02 defines REAL_ratio MUSIC_S1:def 5 :
for b₁ being Function of [:REALPLUS,REALPLUS:],REALPLUS holds
( b₁ = REAL_ratio iff for x being Element of [:REALPLUS,REALPLUS:] ex y, z being Element of REALPLUS st
( x = [y,z] & b₁ . x = REAL_ratio (y,z) ) );