for MS being non empty satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible satisfying_octave_descendent_constructible MusicStruct
for fondamentale, frequency being Element of MS ex seq being sequence of MS st
( seq . 0 = frequency & ( for n being Nat holds seq . (n + 1) = Fifth_reduct (MS,fondamentale,(seq . n)) ) )