defpred S1[ 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 S1[k,x]
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
S1[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
; ( 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; verum