let f1, f2, f3 be Element of RAT_Music; :: thesis: ( the Ratio of RAT_Music . (f1,f1) = the Ratio of RAT_Music . (f2,f3) implies f2 = f3 )
assume A1: the Ratio of RAT_Music . (f1,f1) = the Ratio of RAT_Music . (f2,f3) ; :: thesis: f2 = f3
set S = RAT_Music ;
reconsider x = [f1,f1], y = [f2,f3] as Element of [:RATPLUS,RATPLUS:] by ZFMISC_1:def 2;
consider y9, z9 being Element of RATPLUS such that
A2: x = [y9,z9] and
A3: RAT_ratio . x = RAT_ratio (y9,z9) by Def05;
consider y99, z99 being Element of RATPLUS such that
A4: y = [y99,z99] and
A5: RAT_ratio . y = RAT_ratio (y99,z99) by Def05;
consider r, s being positive Rational such that
A6: ( y9 = r & s = z9 & RAT_ratio (y9,z9) = s / r ) by Def04;
consider r9, s9 being positive Rational such that
A7: ( y99 = r9 & s9 = z99 & RAT_ratio (y99,z99) = s9 / r9 ) by Def04;
A8: ( y9 = f1 & z9 = f1 & y99 = f2 & z99 = f3 ) by A2, A4, XTUPLE_0:1;
( RAT_ratio . (f1,f1) = RAT_ratio (y9,z9) & RAT_ratio . (f2,f3) = RAT_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