let f1, f2, f3, f4 be Element of RAT_Music; :: thesis:
set MS = RAT_Music ;
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;
reconsider x1 = [z9,y9], y1 = [z99,y99] as Element of [:RATPLUS,RATPLUS:] ;
consider y19, z19 being Element of RATPLUS such that
A5: x1 = [y19,z19] and
A6: RAT_ratio . x1 = RAT_ratio (y19,z19) by Def05;
consider y199, z199 being Element of RATPLUS such that
A7: y1 = [y199,z199] and
A8: RAT_ratio . y1 = RAT_ratio (y199,z199) by Def05;
A9: ( f1 = y9 & f2 = z9 & f3 = y99 & f4 = z99 ) by A1, A3, XTUPLE_0:1;
then A10: ( f1 = z19 & f2 = y19 & f3 = z199 & f4 = y199 ) by A5, A7, XTUPLE_0:1;
A11: ( the Ratio of RAT_Music . (f2,f1) = RAT_ratio (y19,z19) & the Ratio of RAT_Music . (f4,f3) = RAT_ratio (y199,z199) ) by A9, BINOP_1:def 1, A6, A8;

hereby :: thesis:

assume A12: 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 A12, A4, BINOP_1:def 1 ;
hence the Ratio of RAT_Music . (f2,f1) = the Ratio of RAT_Music . (f4,f3) by A9, A10, A11, Th13; :: thesis:

end;

assume A13: the Ratio of RAT_Music . (f2,f1) = the Ratio of RAT_Music . (f4,f3) ; :: thesis:
RAT_ratio . (f1,f2) = RAT_ratio (z19,y19) by BINOP_1:def 1, A9, A10, A2
.= RAT_ratio (z199,y199) by A13, A11, Th13
.= RAT_ratio . (f3,f4) by BINOP_1:def 1, A9, A10, A4 ;
hence the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4) ; :: thesis: