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 fondamentale being Element of MS holds (spiral_of_fifths (MS,fondamentale,fondamentale)) . 2 = (9 / 8) * (@ fondamentale)
let fondamentale be Element of MS; :: thesis: (spiral_of_fifths (MS,fondamentale,fondamentale)) . 2 = (9 / 8) * (@ fondamentale)
reconsider n2 = 2, n1 = 1, n0 = 0 as Nat ;
(spiral_of_fifths (MS,fondamentale,fondamentale)) . n1 is Element of MS ;
then reconsider r32 = (3 / 2) * (@ fondamentale) as Element of MS by Th58;
A1: (spiral_of_fifths (MS,fondamentale,fondamentale)) . 2 = (spiral_of_fifths (MS,fondamentale,fondamentale)) . (n1 + 1)
.= Fifth_reduct (MS,fondamentale,((spiral_of_fifths (MS,fondamentale,fondamentale)) . n1)) by Def19
.= Fifth_reduct (MS,fondamentale,r32) by Th58 ;
consider r, s being positive Real such that
A2: ( r = r32 & s = (3 / 2) * r & Fifth (MS,r32) = s ) by Th54;
A3: Fifth (MS,r32) = (9 / 4) * (@ fondamentale) by A2;
A4: ex r being positive Real st
( Fifth (MS,r32) = r & Octave_descendent (MS,(Fifth (MS,r32))) = r / 2 ) by Th51;
not Fifth (MS,r32) is_Between fondamentale, Octave (MS,fondamentale)

proof

assume A5: Fifth (MS,r32) is_Between fondamentale, Octave (MS,fondamentale) ; :: thesis: contradiction
A6: ex fr being positive Real st
( fondamentale = fr & Octave (MS,fondamentale) = 2 * fr ) by Def15;
thus contradiction by A5, A6, A3, XREAL_1:68; :: thesis: verum

end;

hence (spiral_of_fifths (MS,fondamentale,fondamentale)) . 2 = (9 / 8) * (@ fondamentale) by A1, A2, A4, Def18; :: thesis: verum