set MS = REAL_Music ;

now :: thesis: for frequency being Element of REAL_Music ex f, qr being positive Real st
( f = frequency & qr = (1 / 2) * f & [qr,f] in octave REAL_Music )

let frequency be Element of REAL_Music; :: thesis: ex f, qr being positive Real st
( f = frequency & qr = (1 / 2) * f & [qr,f] in octave REAL_Music )
reconsider f = frequency as positive Real by Th1;
reconsider qr = (1 / 2) * f as positive Real ;
reconsider q = qr as Element of REAL_Music by Th1;
take f = f; :: thesis: ex qr being positive Real st
( f = frequency & qr = (1 / 2) * f & [qr,f] in octave REAL_Music )
take qr = qr; :: thesis: ( f = frequency & qr = (1 / 2) * f & [qr,f] in octave REAL_Music )
thus f = frequency ; :: thesis: ( qr = (1 / 2) * f & [qr,f] in octave REAL_Music )
thus qr = (1 / 2) * f ; :: thesis: [qr,f] in octave REAL_Music
reconsider n2 = 2, n3 = 1 as Element of REAL_Music by Th20;
reconsider x = [n2,n3], y = [frequency,q] as Element of [:REALPLUS,REALPLUS:] ;
reconsider z = [frequency,q] as Element of [:REALPLUS,REALPLUS:] ;
consider x9, y9 being Element of REALPLUS such that
A1: z = [x9,y9] and
A2: REAL_ratio . z = REAL_ratio (x9,y9) by Def02;
consider r, s being positive Real such that
A3: ( x9 = r & s = y9 & REAL_ratio (x9,y9) = s / r ) by Def01;
consider x99, y99 being Element of REALPLUS such that
A4: x = [x99,y99] and
A5: REAL_ratio . x = REAL_ratio (x99,y99) by Def02;
consider r9, s9 being positive Real such that
A6: ( x99 = r9 & s9 = y99 & REAL_ratio (x99,y99) = s9 / r9 ) by Def01;
A7: ( n2 = r9 & n3 = s9 & r = frequency & s = q ) by A3, A1, A4, A6, XTUPLE_0:1;

now :: thesis: ( REAL_ratio . (n2,n3) = 1 / 2 & REAL_ratio . (frequency,q) = 1 / 2 )

thus REAL_ratio . (n2,n3) = 1 / 2 by A6, A7, A5, BINOP_1:def 1; :: thesis: REAL_ratio . (frequency,q) = 1 / 2
thus REAL_ratio . (frequency,q) = s / r by A3, A2, BINOP_1:def 1
.= 1 / 2 by A7, XCMPLX_1:89 ; :: thesis: verum

end;

then n2,n3 equiv frequency,q by Def08a;
then n3,n2 equiv q,frequency by Th28;
hence [qr,f] in octave REAL_Music by EQREL_1:18; :: thesis: verum

end;

hence for frequency being Element of REAL_Music ex fr, qr being positive Real st
( fr = frequency & qr = (1 / 2) * fr & [qr,fr] in octave REAL_Music ) ; :: thesis: verum