let p1, p2, p3, p4 be XFinSequence; :: thesis: ( ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ p2) ^ (p3 ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) & ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 )
thus ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ p2) ^ (p3 ^ p4) by AFINSQ_1:27; :: thesis: ( ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) & ((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: ( ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) & ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 )
hence ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) by AFINSQ_1:27; :: thesis: ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4
thus ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 by AFINSQ_1:27; :: thesis: verum