for MS1, MS2 being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for frequency1, fondamentale1 being Element of MS1
for frequency2, fondamentale2 being Element of MS2 st frequency1 = frequency2 & fondamentale1 = fondamentale2 holds
Fifth_reduct (MS1,fondamentale1,frequency1) = Fifth_reduct (MS2,fondamentale2,frequency2)