defpred S₁[ set , set ] means ( ( $1 = 1 implies $2 = frequency ) & ( $1 = 2 implies $2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 ) & ( $1 = 3 implies $2 = (spiral_of_fifths (MS,frequency,frequency)) . 4 ) & ( $1 = 4 implies $2 = (spiral_of_fifths (MS,frequency,frequency)) . 1 ) & ( $1 = 5 implies $2 = (spiral_of_fifths (MS,frequency,frequency)) . 3 ) & ( $1 = 6 implies $2 = Octave (MS,frequency) ) );
A1: for k being Nat st k in Seg 6 holds
ex x being Element of MS st S₁[k,x]

proof

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

end;

consider p being FinSequence of the carrier of MS such that
A2: dom p = Seg 6 and
A3: for k being Nat st k in Seg 6 holds
S₁[k,p . k] from FINSEQ_1:sch 5(A1);
len p = 6 by A2, FINSEQ_1:def 3;
then reconsider p = p as Element of 6 -tuples_on the carrier of MS by FINSEQ_2:92;
take p ; :: thesis: ( p . 1 = frequency & p . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & p . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & p . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & p . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & p . 6 = Octave (MS,frequency) )
( 1 in Seg 6 & 2 in Seg 6 & 3 in Seg 6 & 4 in Seg 6 & 5 in Seg 6 & 6 in Seg 6 ) by FINSEQ_1:1;
hence ( p . 1 = frequency & p . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & p . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & p . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & p . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & p . 6 = Octave (MS,frequency) ) by A3; :: thesis: verum