let MS be MusicSpace; ( 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
; 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 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;
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;
ex qr being positive Real st
( f = frequency & qr = (4 / 3) * f & [f,qr] in fourth MS )take qr =
qr;
( f = frequency & qr = (4 / 3) * f & [f,qr] in fourth MS )thus
f = frequency
;
( qr = (4 / 3) * f & [f,qr] in fourth MS )thus
qr = (4 / 3) * f
;
[f,qr] in fourth MSreconsider 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;
then
n2,
n3 equiv frequency,
q
by A1, Def08a;
hence
[f,qr] in fourth MS
by EQREL_1:18;
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 )
; verum