let MS1, MS2 be non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct ; for frequency1 being Element of MS1
for frequency2 being Element of MS2 st frequency1 = frequency2 holds
Octave_descendent (MS1,frequency1) = Octave_descendent (MS2,frequency2)
let frequency1 be Element of MS1; for frequency2 being Element of MS2 st frequency1 = frequency2 holds
Octave_descendent (MS1,frequency1) = Octave_descendent (MS2,frequency2)
let frequency2 be Element of MS2; ( frequency1 = frequency2 implies Octave_descendent (MS1,frequency1) = Octave_descendent (MS2,frequency2) )
assume A1:
frequency1 = frequency2
; Octave_descendent (MS1,frequency1) = Octave_descendent (MS2,frequency2)
consider r1 being positive Real such that
A2:
( frequency1 = r1 & Octave_descendent (MS1,frequency1) = r1 / 2 )
by Th51;
consider r2 being positive Real such that
A3:
( frequency2 = r2 & Octave_descendent (MS2,frequency2) = r2 / 2 )
by Th51;
thus
Octave_descendent (MS1,frequency1) = Octave_descendent (MS2,frequency2)
by A1, A2, A3; verum