let MS1, MS2 be 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 ; :: thesis: 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)
let frequency1, fondamentale1 be Element of MS1; :: thesis: for frequency2, fondamentale2 being Element of MS2 st frequency1 = frequency2 & fondamentale1 = fondamentale2 holds
Fifth_reduct (MS1,fondamentale1,frequency1) = Fifth_reduct (MS2,fondamentale2,frequency2)
let frequency2, fondamentale2 be Element of MS2; :: thesis: ( frequency1 = frequency2 & fondamentale1 = fondamentale2 implies Fifth_reduct (MS1,fondamentale1,frequency1) = Fifth_reduct (MS2,fondamentale2,frequency2) )
assume that
A1: frequency1 = frequency2 and
A2: fondamentale1 = fondamentale2 ; :: thesis: Fifth_reduct (MS1,fondamentale1,frequency1) = Fifth_reduct (MS2,fondamentale2,frequency2)

per cases ( Fifth (MS1,frequency1) is_Between fondamentale1, Octave (MS1,fondamentale1) or not Fifth (MS1,frequency1) is_Between fondamentale1, Octave (MS1,fondamentale1) ) ;

suppose A3: Fifth (MS1,frequency1) is_Between fondamentale1, Octave (MS1,fondamentale1) ; :: thesis: Fifth_reduct (MS1,fondamentale1,frequency1) = Fifth_reduct (MS2,fondamentale2,frequency2)

then A4: Fifth_reduct (MS1,fondamentale1,frequency1) = Fifth (MS1,frequency1) by Def18;
( Fifth (MS1,frequency1) = Fifth (MS2,frequency2) & fondamentale1 = fondamentale2 & Octave (MS2,fondamentale2) = Octave (MS1,fondamentale1) ) by A1, A2, Th52;
then Fifth (MS2,frequency2) is_Between fondamentale2, Octave (MS2,fondamentale2) by A3;
then Fifth (MS2,frequency2) = Fifth_reduct (MS2,fondamentale2,frequency2) by Def18;
hence Fifth_reduct (MS1,fondamentale1,frequency1) = Fifth_reduct (MS2,fondamentale2,frequency2) by A4, A1, Th52; :: thesis: verum

end;

suppose A5: not Fifth (MS1,frequency1) is_Between fondamentale1, Octave (MS1,fondamentale1) ; :: thesis: Fifth_reduct (MS1,fondamentale1,frequency1) = Fifth_reduct (MS2,fondamentale2,frequency2)

then A6: Fifth_reduct (MS1,fondamentale1,frequency1) = Octave_descendent (MS1,(Fifth (MS1,frequency1))) by Def18;
( Fifth (MS1,frequency1) = Fifth (MS2,frequency2) & fondamentale1 = fondamentale2 & Octave (MS2,fondamentale2) = Octave (MS1,fondamentale1) ) by A1, A2, Th52;
then not Fifth (MS2,frequency2) is_Between fondamentale2, Octave (MS2,fondamentale2) by A5;
then A7: Fifth_reduct (MS2,fondamentale2,frequency2) = Octave_descendent (MS2,(Fifth (MS2,frequency2))) by Def18;
Fifth (MS1,frequency1) = Fifth (MS2,frequency2) by A1, Th52;
hence Fifth_reduct (MS1,fondamentale1,frequency1) = Fifth_reduct (MS2,fondamentale2,frequency2) by A6, A7, Th53; :: thesis: verum

end;

end;