set S = REAL_Music ;

now :: thesis: for frequency being Element of REAL_Music
for n being non zero Nat ex harmonique being Element of REAL_Music st [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n])

let frequency be Element of REAL_Music; :: thesis: for n being non zero Nat ex harmonique being Element of REAL_Music st [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n])
let n be non zero Nat; :: thesis: ex harmonique being Element of REAL_Music st [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n])
reconsider f = frequency as positive Real by Th1;
reconsider harmonique = n * f as Element of REAL_Music by Th1;
take harmonique = harmonique; :: thesis: [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n])
reconsider x = 1, y = n as Element of REAL_Music by Th1;
reconsider z = [x,y] as Element of [:REALPLUS,REALPLUS:] by ZFMISC_1:def 2;
consider x9, y9 being Element of REALPLUS such that
A1: z = [x9,y9] and
A2: REAL_ratio . z = REAL_ratio (x9,y9) by Def02;
reconsider z9 = [frequency,harmonique] as Element of [:REALPLUS,REALPLUS:] by ZFMISC_1:def 2;
consider x99, y99 being Element of REALPLUS such that
A3: z9 = [x99,y99] and
A4: REAL_ratio . z9 = REAL_ratio (x99,y99) by Def02;
consider r, s being positive Real such that
A5: ( x9 = r & s = y9 & REAL_ratio (x9,y9) = s / r ) by Def01;
A6: ( r = 1 & s = n ) by A5, A1, XTUPLE_0:1;
consider r9, s9 being positive Real such that
A7: ( x99 = r9 & s9 = y99 & REAL_ratio (x99,y99) = s9 / r9 ) by Def01;
A8: ( r9 = frequency & s9 = harmonique ) by A7, A3, XTUPLE_0:1;

now :: thesis: ( the Ratio of REAL_Music . (x,y) = n & the Ratio of REAL_Music . (frequency,harmonique) = n )

thus the Ratio of REAL_Music . (x,y) = n by A5, A6, A2, BINOP_1:def 1; :: thesis: the Ratio of REAL_Music . (frequency,harmonique) = n
thus the Ratio of REAL_Music . (frequency,harmonique) = REAL_ratio (x99,y99) by A4, BINOP_1:def 1
.= n by A7, A8, XCMPLX_1:89 ; :: thesis: verum

end;

then x,y equiv frequency,harmonique by Th7;
hence [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n]) by EQREL_1:18; :: thesis: verum

end;

hence for frequency being Element of REAL_Music
for n being non zero Nat ex harmonique being Element of REAL_Music st [frequency,harmonique] in Class ( the Equidistance of REAL_Music,[1,n]) ; :: thesis: verum