theorem Th18: :: MUSIC_S1:22

for f1, f2, fn1, fm1, fn2, fm2 being Element of RAT_Music
for r1, r2 being positive Rational
for n, m being non zero Nat st fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 holds
fn1,fm1 equiv fn2,fm2