:: deftheorem Def19 defines spiral_of_fifths MUSIC_S1:def 53 :
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
for b₄ being sequence of MS holds
( b₄ = spiral_of_fifths (MS,fondamentale,frequency) iff ( b₄ . 0 = frequency & ( for n being Nat holds b₄ . (n + 1) = Fifth_reduct (MS,fondamentale,(b₄ . n)) ) ) );