let f1, f2, fn1, fm1, fn2, fm2 be Element of REAL_Music; :: thesis: for r1, r2 being positive Real
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 Real; :: 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 A0: ( 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 [:REALPLUS,REALPLUS:] by ZFMISC_1:def 2;
consider x9, y9 being Element of REALPLUS such that
A1: z = [x9,y9] and
A2: REAL_ratio . z = REAL_ratio (x9,y9) by Def02;
consider r, s being positive Real such that
A3: ( x9 = r & s = y9 & REAL_ratio (x9,y9) = s / r ) by Def01;
reconsider z9 = [fn2,fm2] as Element of [:REALPLUS,REALPLUS:] by ZFMISC_1:def 2;
consider x99, y99 being Element of REALPLUS such that
A4: z9 = [x99,y99] and
A5: REAL_ratio . z9 = REAL_ratio (x99,y99) by Def02;
consider r9, s9 being positive Real such that
A6: ( x99 = r9 & s9 = y99 & REAL_ratio (x99,y99) = s9 / r9 ) by Def01;

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

thus REAL_ratio . (fn1,fm1) = s / r by A3, A2, BINOP_1:def 1; :: thesis: ( REAL_ratio . (fn2,fm2) = s9 / r9 & s / r = s9 / r9 )
thus REAL_ratio . (fn2,fm2) = s9 / r9 by A6, A5, BINOP_1:def 1; :: thesis: s / r = s9 / r9
( r = n * r1 & s = m * r1 & r9 = n * r2 & s9 = m * r2 ) by A4, A6, A1, A3, A0, 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 Th7; :: 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