theorem Th32: :: FINSEQ_1:32

for p, q, r being FinSequence holds (p ^ q) ^ r = p ^ (q ^ r)