let MS 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 frequency being Element of MS holds (@ ((spiral_of_fifths (MS,frequency,frequency)) . 3)) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 1)) = 9 / 8
let frequency be Element of MS; :: thesis: (@ ((spiral_of_fifths (MS,frequency,frequency)) . 3)) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 1)) = 9 / 8
( (spiral_of_fifths (MS,frequency,frequency)) . 3 = (27 / 16) * (@ frequency) & (spiral_of_fifths (MS,frequency,frequency)) . 1 = (3 / 2) * (@ frequency) ) by Th58, Th60;
then (@ ((spiral_of_fifths (MS,frequency,frequency)) . 3)) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 1)) = (27 / 16) / (3 / 2) by XCMPLX_1:91
.= 9 / 8 ;
hence (@ ((spiral_of_fifths (MS,frequency,frequency)) . 3)) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 1)) = 9 / 8 ; :: thesis: verum