set MS = HPS;
defpred S1[ set , set ] means ( ( $1 = 1 implies $2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 ) & ( $1 = 2 implies $2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 ) & ( $1 = 3 implies $2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 ) & ( $1 = 4 implies $2 = Fourth (HPS,frequency) ) & ( $1 = 5 implies $2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 ) & ( $1 = 6 implies $2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 ) & ( $1 = 7 implies $2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 ) & ( $1 = 8 implies $2 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) ) );
A1:
for k being Nat st k in Seg 8 holds
ex x being Element of HPS st S1[k,x]
consider p being FinSequence of the carrier of HPS such that
A2:
dom p = Seg 8
and
A3:
for k being Nat st k in Seg 8 holds
S1[k,p . k]
from FINSEQ_1:sch 5(A1);
len p = 8
by A2, FINSEQ_1:def 3;
then reconsider p = p as Element of 8 -tuples_on the carrier of HPS by FINSEQ_2:92;
take
p
; ( p . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & p . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & p . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & p . 4 = Fourth (HPS,frequency) & p . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & p . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & p . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & p . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) )
( 1 in Seg 8 & 2 in Seg 8 & 3 in Seg 8 & 4 in Seg 8 & 5 in Seg 8 & 6 in Seg 8 & 7 in Seg 8 & 8 in Seg 8 )
by FINSEQ_1:1;
hence
( p . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & p . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & p . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & p . 4 = Fourth (HPS,frequency) & p . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & p . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & p . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & p . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) )
by A3; verum