reconsider MS = REAL_Music as satisfying_fourth_constructible MusicSpace by Th79;
A1:
MS is classical_fourth
by Th80;
now for f1, f2 being Element of REAL_Music holds the Ratio of REAL_Music . (f1,f2) = (@ f2) / (@ f1)let f1,
f2 be
Element of
REAL_Music;
the Ratio of REAL_Music . (f1,f2) = (@ f2) / (@ f1)reconsider x =
[f1,f2] as
Element of
[:REALPLUS,REALPLUS:] ;
consider y9,
z9 being
Element of
REALPLUS such that A2:
x = [y9,z9]
and A3:
REAL_ratio . x = REAL_ratio (
y9,
z9)
by Def02;
consider y99,
z99 being
Element of
REALPLUS such that A4:
x = [y99,z99]
and
REAL_ratio . x = REAL_ratio (
y99,
z99)
by Def02;
consider r,
s being
positive Real such that A5:
(
y99 = r &
s = z99 &
REAL_ratio (
y99,
z99)
= s / r )
by Def01;
A6:
(
s = @ f2 &
r = @ f1 )
by A5, A4, XTUPLE_0:1;
A7:
(
y99 = y9 &
z99 = z9 )
by A2, A4, XTUPLE_0:1;
thus
the
Ratio of
REAL_Music . (
f1,
f2)
= (@ f2) / (@ f1)
by A7, A5, A3, BINOP_1:def 1, A6;
verum end;
then
MS is satisfying_euclidean
;
hence
ex b1 being satisfying_fourth_constructible classical_fourth MusicSpace st b1 is satisfying_euclidean
by A1; verum