set MS = RAT_Music ;

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

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

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

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

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

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

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

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

end;

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

end;

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

end;

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

end;

hence RAT_Music is satisfying_linearite_harmonique ; :: thesis: verum