let MS be MusicSpace; :: thesis:
let frequency be Element of MS; :: thesis:
set scale = pentatonic_pythagorean_scale (MS,frequency);
A1: ( (pentatonic_pythagorean_scale (MS,frequency)) . 1 = frequency & (pentatonic_pythagorean_scale (MS,frequency)) . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & (pentatonic_pythagorean_scale (MS,frequency)) . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & (pentatonic_pythagorean_scale (MS,frequency)) . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & (pentatonic_pythagorean_scale (MS,frequency)) . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & (pentatonic_pythagorean_scale (MS,frequency)) . 6 = Octave (MS,frequency) ) by Def20;
pentatonic_pythagorean_scale (MS,frequency) in 6 -tuples_on the carrier of MS ;
then pentatonic_pythagorean_scale (MS,frequency) in { s where s is Element of the carrier of MS * : len s = 6 } by FINSEQ_2:def 4;
then consider s being Element of the carrier of MS * such that
A2: s = pentatonic_pythagorean_scale (MS,frequency) and
A3: len s = 6 ;
dom s = Seg 6 by A3, FINSEQ_1:def 3;
then reconsider g1 = (pentatonic_pythagorean_scale (MS,frequency)) . 1, g2 = (pentatonic_pythagorean_scale (MS,frequency)) . 2, g3 = (pentatonic_pythagorean_scale (MS,frequency)) . 3, g4 = (pentatonic_pythagorean_scale (MS,frequency)) . 4, g5 = (pentatonic_pythagorean_scale (MS,frequency)) . 5, g6 = (pentatonic_pythagorean_scale (MS,frequency)) . 6 as Element of the carrier of MS by A2, FINSEQ_1:1, FINSEQ_2:11;

now :: thesis:

reconsider frequency = g1 as Element of MS ;
take frequency = frequency; :: thesis:
reconsider r1 = @ frequency, r2 = @ g2, r3 = @ g3, r4 = @ g4, r5 = @ g5, r6 = @ g6 as positive Real ;
take r1 = r1; :: thesis:
take r2 = r2; :: thesis:
take r3 = r3; :: thesis:
take r4 = r4; :: thesis:
take r5 = r5; :: thesis:
take r6 = r6; :: thesis:
thus ( (pentatonic_pythagorean_scale (MS,frequency)) . 1 = frequency & (pentatonic_pythagorean_scale (MS,frequency)) . 1 = r1 & (pentatonic_pythagorean_scale (MS,frequency)) . 2 = r2 & (pentatonic_pythagorean_scale (MS,frequency)) . 3 = r3 & (pentatonic_pythagorean_scale (MS,frequency)) . 4 = r4 & (pentatonic_pythagorean_scale (MS,frequency)) . 5 = r5 & (pentatonic_pythagorean_scale (MS,frequency)) . 6 = r6 ) ; :: thesis:

now :: thesis:

thus r1 = 1 * (@ frequency) ; :: thesis:
thus r2 = (9 / 8) * (@ frequency) by Th59, A1; :: thesis:
thus r3 = (81 / 64) * (@ frequency) by A1, Th61; :: thesis:
thus r4 = (3 / 2) * (@ frequency) by A1, Th58; :: thesis:
thus r5 = (27 / 16) * (@ frequency) by A1, Th60; :: thesis:
ex fr being positive Real st
( frequency = fr & Octave (MS,frequency) = 2 * fr ) by Def15;
hence r6 = 2 * (@ frequency) by A1; :: thesis:

end;

hence ( r1 < r2 & r2 < r3 & r3 < r4 & r4 < r5 & r5 < r6 ) by XREAL_1:68; :: thesis:
thus (pentatonic_pythagorean_scale (MS,frequency)) . 6 = Octave (MS,frequency) by A1; :: thesis:

end;

hence pentatonic_pythagorean_scale (MS,frequency) is pentatonic ; :: thesis: