reconsider MS = REAL_Music as MusicSpace ;

now :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

then MS is satisfying_euclidean ;
hence ex b₁ being non empty satisfying_Real MusicStruct st b₁ is satisfying_euclidean ; :: thesis: verum