theorem Th91: :: MUSIC_S1:113

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds
( (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1 = 2 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2 = (9 / 4) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3 = (81 / 32) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4 = (8 / 3) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 5 = 3 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 6 = (27 / 8) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 7 = (243 / 64) * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 8 = 4 * (@ frequency) )