for MS1, MS2 being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave MusicStruct
for f1 being Element of MS1
for f2 being Element of MS2 st f1 = f2 holds
( Fifth (MS1,f1) = Fifth (MS2,f2) & Octave (MS1,f1) = Octave (MS2,f2) )