let f1, f2, f3 be Element of REAL_Music; ( 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)
; 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; verum