set T = RAT_Music ;
thus not RAT_Music is empty ; :: thesis:
thus the carrier of RAT_Music c= REALPLUS by Th5; :: thesis:
thus for f1, f2, f3, f4 being Element of RAT_Music holds
( f1,f2 equiv f3,f4 iff the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4) ) :: thesis:

proof

let f1, f2, f3, f4 be Element of RAT_Music; :: thesis:
reconsider x = [f1,f2], y = [f3,f4] as Element of [:RATPLUS,RATPLUS:] by ZFMISC_1:def 2;
consider y9, z9 being Element of RATPLUS such that
A1: x = [y9,z9] and
A2: RAT_ratio . x = RAT_ratio (y9,z9) by Def05;
consider y99, z99 being Element of RATPLUS such that
A3: y = [y99,z99] and
A4: RAT_ratio . y = RAT_ratio (y99,z99) by Def05;

hereby :: thesis:

assume f1,f2 equiv f3,f4 ; :: thesis:
then consider a, b, c, d being Element of RATPLUS such that
A5: ( x = [a,b] & y = [c,d] ) and
A6: RAT_ratio (a,b) = RAT_ratio (c,d) by Def06;
( y9 = a & z9 = b & y99 = c & z99 = d ) by A1, A3, A5, XTUPLE_0:1;
then ( a = f1 & b = f2 & c = f3 & d = f4 & the Ratio of RAT_Music . (a,b) = RAT_ratio (a,b) & the Ratio of RAT_Music . (c,d) = RAT_ratio (c,d) ) by XTUPLE_0:1, A2, A4, A5, BINOP_1:def 1;
hence the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4) by A6; :: thesis:

end;

assume A7: the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4) ; :: thesis:
RAT_ratio (y9,z9) = RAT_ratio . (f1,f2) by A2, BINOP_1:def 1
.= RAT_ratio (y99,z99) by A7, A4, BINOP_1:def 1 ;
hence f1,f2 equiv f3,f4 by A1, A3, Def06; :: thesis:

end;