let frequency be Element of RAT_Music; :: thesis:
reconsider f = frequency as positive Rational by Th2;
reconsider qr = 2 * f as positive Rational ;
reconsider q = qr as Element of RAT_Music by Th2;
take f = f; :: thesis:
take qr = qr; :: thesis:
thus f = frequency ; :: thesis:
thus qr = 2 * f ; :: thesis:
reconsider n2 = 1, n3 = 2 as Element of RAT_Music by Th20;
reconsider x = [n2,n3], y = [frequency,q] as Element of [:RATPLUS,RATPLUS:] ;
reconsider z = [frequency,q] as Element of [:RATPLUS,RATPLUS:] ;
consider x9, y9 being Element of RATPLUS such that
A1: z = [x9,y9] and
A2: RAT_ratio . z = RAT_ratio (x9,y9) by Def05;
consider r, s being positive Rational such that
A3: ( x9 = r & s = y9 & RAT_ratio (x9,y9) = s / r ) by Def04;
consider x99, y99 being Element of RATPLUS such that
A4: x = [x99,y99] and
A5: RAT_ratio . x = RAT_ratio (x99,y99) by Def05;
consider r9, s9 being positive Rational such that
A6: ( x99 = r9 & s9 = y99 & RAT_ratio (x99,y99) = s9 / r9 ) by Def04;
A7: ( n2 = r9 & n3 = s9 & r = frequency & s = q ) by A3, A1, A4, A6, XTUPLE_0:1;

end;

end;