let f1, f2, fn1, fm1, fn2, fm2 be Element of RAT_Music; :: thesis: 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
let r1, r2 be positive Rational; :: thesis: 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

now :: thesis: 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

let n, m be non zero Nat; :: thesis: ( fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 implies fn1,fm1 equiv fn2,fm2 )
assume A1: ( fn1 = n * r1 & fm1 = m * r1 & fn2 = n * r2 & fm2 = m * r2 ) ; :: thesis: fn1,fm1 equiv fn2,fm2
reconsider z = [fn1,fm1] as Element of [:RATPLUS,RATPLUS:] by ZFMISC_1:def 2;
consider x9, y9 being Element of RATPLUS such that
A2: z = [x9,y9] and
A3: RAT_ratio . z = RAT_ratio (x9,y9) by Def05;
consider r, s being positive Rational such that
A4: ( x9 = r & s = y9 & RAT_ratio (x9,y9) = s / r ) by Def04;
reconsider z9 = [fn2,fm2] as Element of [:RATPLUS,RATPLUS:] by ZFMISC_1:def 2;
consider x99, y99 being Element of RATPLUS such that
A5: z9 = [x99,y99] and
A6: RAT_ratio . z9 = RAT_ratio (x99,y99) by Def05;
consider r9, s9 being positive Rational such that
A7: ( x99 = r9 & s9 = y99 & RAT_ratio (x99,y99) = s9 / r9 ) by Def04;

now :: thesis: ( RAT_ratio . (fn1,fm1) = s / r & RAT_ratio . (fn2,fm2) = s9 / r9 & s / r = s9 / r9 )

thus RAT_ratio . (fn1,fm1) = s / r by A3, A4, BINOP_1:def 1; :: thesis: ( RAT_ratio . (fn2,fm2) = s9 / r9 & s / r = s9 / r9 )
thus RAT_ratio . (fn2,fm2) = s9 / r9 by A6, A7, BINOP_1:def 1; :: thesis: s / r = s9 / r9
( r = n * r1 & s = m * r1 & r9 = n * r2 & s9 = m * r2 ) by A1, A2, A4, A5, A7, XTUPLE_0:1;
then ( s / r = m / n & s9 / r9 = m / n ) by XCMPLX_1:91;
hence s / r = s9 / r9 ; :: thesis: verum

end;

hence fn1,fm1 equiv fn2,fm2 by Th14; :: thesis: verum

end;

hence 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 ; :: thesis: verum