let MS1, MS2 be satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave MusicStruct ; :: thesis: 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) )
let f1 be Element of MS1; :: thesis: for f2 being Element of MS2 st f1 = f2 holds
( Fifth (MS1,f1) = Fifth (MS2,f2) & Octave (MS1,f1) = Octave (MS2,f2) )
let f2 be Element of MS2; :: thesis: ( f1 = f2 implies ( Fifth (MS1,f1) = Fifth (MS2,f2) & Octave (MS1,f1) = Octave (MS2,f2) ) )
assume A1: f1 = f2 ; :: thesis: ( Fifth (MS1,f1) = Fifth (MS2,f2) & Octave (MS1,f1) = Octave (MS2,f2) )
consider fr1 being positive Real such that
A2: ( f1 = fr1 & Fifth (MS1,f1) = (3 / 2) * fr1 ) by Def12;
consider fr2 being positive Real such that
A3: ( f2 = fr2 & Fifth (MS2,f2) = (3 / 2) * fr2 ) by Def12;
thus Fifth (MS1,f1) = Fifth (MS2,f2) by A1, A2, A3; :: thesis: Octave (MS1,f1) = Octave (MS2,f2)
( ex fr being positive Real st
( f1 = fr & Octave (MS1,f1) = 2 * fr ) & ex fr being positive Real st
( f2 = fr & Octave (MS2,f2) = 2 * fr ) ) by Def15;
hence Octave (MS1,f1) = Octave (MS2,f2) by A1; :: thesis: verum