theorem Th25: :: AFINSQ_1:27

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