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

proof

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

hereby :: thesis:

assume f1,f2 equiv f3,f4 ; :: thesis:
then consider a, b, c, d being Element of REALPLUS such that
A5: ( x = [a,b] & y = [c,d] ) and
A6: REAL_ratio (a,b) = REAL_ratio (c,d) by Def03;
( 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 REAL_Music . (a,b) = REAL_ratio (a,b) & the Ratio of REAL_Music . (c,d) = REAL_ratio (c,d) ) by XTUPLE_0:1, A2, A4, A5, BINOP_1:def 1;
hence the Ratio of REAL_Music . (f1,f2) = the Ratio of REAL_Music . (f3,f4) by A6; :: thesis:

end;

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

end;