set MS = REAL_Music ;

now :: thesis: for frequency being Element of REAL_Music
for n being non zero Nat ex fr being positive Real st
( frequency = fr & n -harmonique (REAL_Music,frequency) = n * fr )

let frequency be Element of REAL_Music; :: thesis: for n being non zero Nat ex fr being positive Real st
( frequency = fr & n -harmonique (REAL_Music,frequency) = n * fr )
let n be non zero Nat; :: thesis: ex fr being positive Real st
( frequency = fr & n -harmonique (REAL_Music,frequency) = n * fr )
reconsider fr = frequency as positive Real by Th1;
take fr = fr; :: thesis: ( frequency = fr & n -harmonique (REAL_Music,frequency) = n * fr )
thus frequency = fr ; :: thesis: n -harmonique (REAL_Music,frequency) = n * fr
reconsider n1 = 1, n2 = n as Element of REAL_Music by Th20;
reconsider f2 = n * fr as Element of REAL_Music by Th1;
reconsider x = [n1,n2], y = [frequency,f2] as Element of [:REALPLUS,REALPLUS:] ;

now :: thesis: ( [frequency,(n -harmonique (REAL_Music,frequency))] in Class ( the Equidistance of REAL_Music,[1,n]) & [frequency,f2] in Class ( the Equidistance of REAL_Music,[1,n]) )

thus [frequency,(n -harmonique (REAL_Music,frequency))] in Class ( the Equidistance of REAL_Music,[1,n]) by Def08b; :: thesis: [frequency,f2] in Class ( the Equidistance of REAL_Music,[1,n])

now :: thesis: ( the Ratio of REAL_Music . (n1,n2) = REAL_ratio . (n1,n2) & the Ratio of REAL_Music . (frequency,f2) = REAL_ratio . (frequency,f2) & REAL_ratio . (n1,n2) = REAL_ratio . (frequency,f2) )

thus the Ratio of REAL_Music . (n1,n2) = REAL_ratio . (n1,n2) ; :: thesis: ( the Ratio of REAL_Music . (frequency,f2) = REAL_ratio . (frequency,f2) & REAL_ratio . (n1,n2) = REAL_ratio . (frequency,f2) )
thus the Ratio of REAL_Music . (frequency,f2) = REAL_ratio . (frequency,f2) ; :: thesis: REAL_ratio . (n1,n2) = REAL_ratio . (frequency,f2)

now :: thesis: ( REAL_ratio . (n1,n2) = n & REAL_ratio . (frequency,f2) = n )

reconsider n19 = n1, n29 = n2, fr9 = fr, f29 = f2 as Element of REALPLUS ;
consider r, s being positive Real such that
A1: ( n19 = r & n29 = s & REAL_ratio (n19,n29) = s / r ) by Def01;
consider r9, s9 being positive Real such that
A2: ( fr9 = r9 & f29 = s9 & REAL_ratio (fr9,f29) = s9 / r9 ) by Def01;
consider y9, z9 being Element of REALPLUS such that
A3: x = [y9,z9] and
A4: REAL_ratio . x = REAL_ratio (y9,z9) by Def02;
consider y99, z99 being Element of REALPLUS such that
A5: y = [y99,z99] and
A6: REAL_ratio . y = REAL_ratio (y99,z99) by Def02;
A7: ( y9 = n1 & z9 = n2 & y99 = frequency & z99 = f2 ) by A3, A5, XTUPLE_0:1;
hence REAL_ratio . (n1,n2) = n by A1, A4, BINOP_1:def 1; :: thesis: REAL_ratio . (frequency,f2) = n
thus REAL_ratio . (frequency,f2) = s9 / r9 by A2, A7, A6, BINOP_1:def 1
.= n by A2, XCMPLX_1:89 ; :: thesis: verum

end;

hence REAL_ratio . (n1,n2) = REAL_ratio . (frequency,f2) ; :: thesis: verum

end;

then n1,n2 equiv frequency,f2 by Def08a;
hence [frequency,f2] in Class ( the Equidistance of REAL_Music,[1,n]) by EQREL_1:18; :: thesis: verum

end;

hence n -harmonique (REAL_Music,frequency) = n * fr by Def08b; :: thesis: verum

end;

hence REAL_Music is satisfying_linearite_harmonique ; :: thesis: verum