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 ; 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; 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; ( frequency1 = frequency2 & fondamentale1 = fondamentale2 implies Fifth_reduct (MS1,fondamentale1,frequency1) = Fifth_reduct (MS2,fondamentale2,frequency2) )
assume that
A1:
frequency1 = frequency2
and
A2:
fondamentale1 = fondamentale2
; 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)
;
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;
verum end; suppose A5:
not
Fifth (
MS1,
frequency1)
is_Between fondamentale1,
Octave (
MS1,
fondamentale1)
;
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;
verum end; end;