theorem Th7: :: MUSIC_S1:8

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