let f1, f2, f3 be Element of REAL_Music; :: thesis: ( the Ratio of REAL_Music . (f1,f1) = the Ratio of REAL_Music . (f2,f3) implies f2 = f3 )
assume A1: the Ratio of REAL_Music . (f1,f1) = the Ratio of REAL_Music . (f2,f3) ; :: thesis: f2 = f3
reconsider x = [f1,f1], y = [f2,f3] as Element of [:REALPLUS,REALPLUS:] by ZFMISC_1:def 2;
consider y9, z9 being Element of REALPLUS such that
A2: x = [y9,z9] and
A3: REAL_ratio . x = REAL_ratio (y9,z9) by Def02;
consider y99, z99 being Element of REALPLUS such that
A4: y = [y99,z99] and
A5: REAL_ratio . y = REAL_ratio (y99,z99) by Def02;
consider r, s being positive Real such that
A6: ( y9 = r & s = z9 & REAL_ratio (y9,z9) = s / r ) by Def01;
consider r9, s9 being positive Real such that
A7: ( y99 = r9 & s9 = z99 & REAL_ratio (y99,z99) = s9 / r9 ) by Def01;
A8: ( y9 = f1 & z9 = f1 & y99 = f2 & z99 = f3 ) by A2, A4, XTUPLE_0:1;
( REAL_ratio . (f1,f1) = REAL_ratio (y9,z9) & REAL_ratio . (f2,f3) = REAL_ratio (y99,z99) ) by A5, A3, BINOP_1:def 1;
hence f2 = f3 by A7, A8, XCMPLX_1:58, XCMPLX_1:60, A6, A1; :: thesis: verum