theorem Th9: :: MUSIC_S1:11

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])