theorem Th14: :: MUSIC_S1:16

( not RAT_Music is empty & the carrier of RAT_Music c= REALPLUS & ( for f1, f2, f3, f4 being Element of RAT_Music holds
( f1,f2 equiv f3,f4 iff the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4) ) ) )