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 ; :: thesis: 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; :: thesis: for frequency2 being Element of MS2 st frequency1 = frequency2 holds
Octave_descendent (MS1,frequency1) = Octave_descendent (MS2,frequency2)
let frequency2 be Element of MS2; :: thesis: ( frequency1 = frequency2 implies Octave_descendent (MS1,frequency1) = Octave_descendent (MS2,frequency2) )
assume A1: frequency1 = frequency2 ; :: thesis: 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; :: thesis: verum