set MS = HPS;
defpred S₁[ 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 S₁[k,x]

let k be Nat; :: thesis:
assume k in Seg 8 ; :: thesis:
then ( 1 <= k & k <= 8 ) by FINSEQ_1:1;
then not not k = 1 & ... & not k = 8 ;
hence ex x being Element of HPS st S₁[k,x] ; :: thesis:

end;

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
S₁[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 ; :: thesis:
( 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; :: thesis: