:: deftheorem Def09 defines satisfying_linearite_harmonique MUSIC_S1:def 20 :
for S being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed MusicStruct holds
( S is satisfying_linearite_harmonique iff for frequency being Element of S
for n being non zero Nat ex fr being positive Real st
( frequency = fr & n -harmonique (S,frequency) = n * fr ) );