let MS be MusicSpace; :: thesis: ( MS = REAL_Music implies for frequency being Element of MS ex fr, qr being positive Real st
( fr = frequency & qr = (4 / 3) * fr & [fr,qr] in fourth MS ) )
assume A1: MS = REAL_Music ; :: thesis: for frequency being Element of MS ex fr, qr being positive Real st
( fr = frequency & qr = (4 / 3) * fr & [fr,qr] in fourth MS )

now :: thesis: for frequency being Element of MS ex f, qr being positive Real st
( f = frequency & qr = (4 / 3) * f & [f,qr] in fourth MS )

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

now :: thesis: ( REAL_ratio . (n2,n3) = 4 / 3 & REAL_ratio . (frequency,q) = 4 / 3 )

thus REAL_ratio . (n2,n3) = 4 / 3 by A7, A8, A6, BINOP_1:def 1; :: thesis: REAL_ratio . (frequency,q) = 4 / 3
thus REAL_ratio . (frequency,q) = s / r by A3, A4, BINOP_1:def 1
.= 4 / 3 by A8, XCMPLX_1:89 ; :: thesis: verum

end;

then n2,n3 equiv frequency,q by A1, Def08a;
hence [f,qr] in fourth MS by EQREL_1:18; :: thesis: verum

end;

hence for frequency being Element of MS ex fr, qr being positive Real st
( fr = frequency & qr = (4 / 3) * fr & [fr,qr] in fourth MS ) ; :: thesis: verum