theorem Th2: :: POLNOT_1:2

for P, Q, R being FinSequence-membered set holds (P ^ Q) ^ R = P ^ (Q ^ R)