:: deftheorem Def28 defines # MUSIC_S1:def 91 :
for HPS being MusicSpace
for n being natural non zero Number
for scale being Element of n -tuples_on the carrier of HPS
for i being Nat holds
( ( i in Seg n implies # (scale,i) = scale . i ) & ( not i in Seg n implies # (scale,i) = the Element of HPS ) );