set MS = REAL_Music ;
now 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;
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;
ex qr being positive Real st
( f = frequency & qr = (1 / 2) * f & [qr,f] in octave REAL_Music )take qr =
qr;
( f = frequency & qr = (1 / 2) * f & [qr,f] in octave REAL_Music )thus
f = frequency
;
( qr = (1 / 2) * f & [qr,f] in octave REAL_Music )thus
qr = (1 / 2) * f
;
[qr,f] in octave REAL_Musicreconsider 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;
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;
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 )
; verum