set MS = HPS;
let p1, p2 be Element of 8 -tuples_on the carrier of HPS; :: thesis: ( p1 . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & p1 . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & p1 . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & p1 . 4 = Fourth (HPS,frequency) & p1 . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & p1 . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & p1 . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & p1 . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) & p2 . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & p2 . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & p2 . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & p2 . 4 = Fourth (HPS,frequency) & p2 . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & p2 . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & p2 . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & p2 . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) implies p1 = p2 )
assume that
A4: ( p1 . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & p1 . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & p1 . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & p1 . 4 = Fourth (HPS,frequency) & p1 . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & p1 . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & p1 . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & p1 . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) ) and
A5: ( p2 . 1 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1 & p2 . 2 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 3 & p2 . 3 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 5 & p2 . 4 = Fourth (HPS,frequency) & p2 . 5 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 & p2 . 6 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 4 & p2 . 7 = (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 6 & p2 . 8 = Octave (HPS,((spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 1)) ) ; :: 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 = 8 & len p2 = 8 ) by FINSEQ_2:132;
then ( dom p1 = Seg 8 & dom p2 = Seg 8 ) 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 8 by FINSEQ_2:132;
then ( 1 <= j & j <= 8 ) by FINSEQ_1:1;
then not not j = 1 & ... & not j = 8 ;
hence p1 . i = p2 . i by A4, A5; :: thesis: verum

end;

end;

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