let p1, p2, p3, p4 be XFinSequence; :: thesis: ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4)
thus ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 by AFINSQ_1:27
.= p1 ^ ((p2 ^ p3) ^ p4) by AFINSQ_1:27 ; :: thesis: verum