reconsider MS = REAL_Music as MusicSpace ;
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 A1:
x = [y9,z9]
and A2:
REAL_ratio . x = REAL_ratio (
y9,
z9)
by Def02;
consider y99,
z99 being
Element of
REALPLUS such that A3:
x = [y99,z99]
and
REAL_ratio . x = REAL_ratio (
y99,
z99)
by Def02;
consider r,
s being
positive Real such that A4:
(
y99 = r &
s = z99 &
REAL_ratio (
y99,
z99)
= s / r )
by Def01;
A5:
(
s = @ f2 &
r = @ f1 )
by A4, A3, XTUPLE_0:1;
A6:
(
y99 = y9 &
z99 = z9 )
by A1, A3, XTUPLE_0:1;
thus
the
Ratio of
REAL_Music . (
f1,
f2)
= (@ f2) / (@ f1)
by A2, BINOP_1:def 1, A5, A6, A4;
verum end;
then
MS is satisfying_euclidean
;
hence
ex b1 being non empty satisfying_Real MusicStruct st b1 is satisfying_euclidean
; verum