let p1, p2 be Element of 6 -tuples_on the carrier of MS; :: thesis: ( p1 . 1 = frequency & p1 . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & p1 . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & p1 . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & p1 . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & p1 . 6 = Octave (MS,frequency) & p2 . 1 = frequency & p2 . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & p2 . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & p2 . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & p2 . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & p2 . 6 = Octave (MS,frequency) implies p1 = p2 )
assume that
A4: ( p1 . 1 = frequency & p1 . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & p1 . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & p1 . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & p1 . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & p1 . 6 = Octave (MS,frequency) ) and
A5: ( p2 . 1 = frequency & p2 . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & p2 . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & p2 . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & p2 . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & p2 . 6 = Octave (MS,frequency) ) ; :: thesis: p1 = p2

now :: thesis: ( dom p1 = dom p2 & ( for i being object st i in dom p1 holds
p1 . i = p2 . i ) )

( len p1 = 6 & len p2 = 6 ) by FINSEQ_2:132;
then ( dom p1 = Seg 6 & dom p2 = Seg 6 ) by FINSEQ_1:def 3;
hence dom p1 = dom p2 ; :: thesis: for i being object st i in dom p1 holds
p1 . i = p2 . i

hereby :: thesis: verum

let i be object ; :: thesis: ( i in dom p1 implies p1 . i = p2 . i )
assume A6: i in dom p1 ; :: thesis: p1 . i = p2 . i
then reconsider j = i as Nat ;
j in Seg (len p1) by A6, FINSEQ_1:def 3;
then j in Seg 6 by FINSEQ_2:132;
then ( 1 <= j & j <= 6 ) by FINSEQ_1:1;
then not not j = 1 & ... & not j = 6 ;
hence p1 . i = p2 . i by A4, A5; :: thesis: verum

end;

end;

hence p1 = p2 by FUNCT_1:def 11; :: thesis: verum